1
2
3
4 package net.sf.bddbddb;
5
6 import java.util.Collection;
7 import java.util.HashSet;
8 import java.util.Iterator;
9 import java.util.LinkedList;
10 import java.util.List;
11 import java.util.NoSuchElementException;
12 import java.util.Set;
13 import java.io.BufferedWriter;
14 import java.io.FileReader;
15 import java.io.FileWriter;
16 import java.io.IOException;
17 import java.io.InputStream;
18 import java.io.InputStreamReader;
19 import java.io.LineNumberReader;
20 import java.io.PrintStream;
21 import jwutil.io.SystemProperties;
22 import net.sf.bddbddb.Solver.MyReader;
23
24 /***
25 * Command-line interactive bddbddb solver.
26 *
27 * The command line accepts anything that is valid in a Datalog file, plus
28 * a special query syntax that ends with '?'. Queries cause the solver to
29 * automatically solve the Datalog with respect to the given query. There
30 * are also some extra commands; type "help" to get a list of them.
31 *
32 * @author jwhaley
33 * @version $Id: Interactive.java 642 2006-06-08 02:35:35Z joewhaley $
34 */
35 public class Interactive {
36
37 public static InputStream in = System.in;
38 public static PrintStream out = System.out;
39 public static PrintStream err = System.err;
40
41 public static boolean IGNORE_OUTPUT = !SystemProperties.getProperty("ignoreoutput", "yes").equals("no");
42
43 /***
44 * Solver we are using.
45 */
46 protected Solver solver;
47
48 /***
49 * Datalog parser.
50 */
51 protected DatalogParser parser;
52
53 /***
54 * Construct a new interactive solver.
55 *
56 * @param s solver to use
57 */
58 public Interactive(Solver s) {
59 this.solver = s;
60 this.solver.out = out;
61 this.solver.err = err;
62 }
63
64 /***
65 * The entry point of the application.
66 *
67 * @param args command line args
68 * @throws InstantiationException
69 * @throws IllegalAccessException
70 * @throws ClassNotFoundException
71 * @throws IOException
72 */
73 public static void main(String[] args) throws InstantiationException, IllegalAccessException, ClassNotFoundException, IOException {
74 String solverName = SystemProperties.getProperty("solver", "net.sf.bddbddb.BDDSolver");
75 Solver dis = (Solver) Class.forName(solverName).newInstance();
76 String file = "";
77 if (args.length > 0) {
78 file = args[0];
79 }
80 dis.initializeBasedir(file);
81 Interactive a = new Interactive(dis);
82 a.parser = new DatalogParser(dis);
83 if (file.length() > 0) {
84 MyReader in = new MyReader(new LineNumberReader(new FileReader(file)));
85 out.println("Reading "+file+"...");
86 a.parser.readDatalogProgram(in);
87 in.close();
88 }
89 if (IGNORE_OUTPUT) {
90 dis.relationsToDump.clear();
91 dis.relationsToDumpTuples.clear();
92 dis.relationsToPrintSize.clear();
93 dis.relationsToPrintTuples.clear();
94 }
95 out.println("Welcome to the interactive bddbddb Datalog solver!");
96 out.println("Type a Datalog rule or query, or \"help\" for help.");
97 a.interactive();
98 }
99
100 /***
101 * Utility function to read a line from the given reader.
102 * Allows line wrapping using backslashes, among other things.
103 *
104 * @param in input reader
105 * @return line
106 * @throws IOException
107 */
108 static String readLine(MyReader in) throws IOException {
109 String s = in.readLine();
110 if (s == null) return null;
111 s = s.trim();
112 while (s.endsWith("//")) {
113 String s2 = in.readLine();
114 if (s2 == null) break;
115 s2 = s2.trim();
116 s = s.substring(0, s.length() - 1) + s2;
117 }
118 return s;
119 }
120
121 /***
122 * Flag to record whether or not we need to call the solver again.
123 */
124 boolean changed = false;
125
126 /***
127 * Log of what has been typed so far.
128 */
129 List log;
130
131 /***
132 * Dump the log to a file.
133 *
134 * @throws IOException
135 */
136 void dumpLog() throws IOException {
137 BufferedWriter w = null;
138 try {
139 w = new BufferedWriter(new FileWriter("bddbddb.log"));
140 for (Iterator i = log.iterator(); i.hasNext(); ) {
141 w.write(i.next()+"\n");
142 }
143 } finally {
144 if (w != null) try { w.close(); } catch (IOException _) { }
145 }
146 }
147
148 /***
149 * Print the log.
150 */
151 void printLog() {
152 for (Iterator i = log.iterator(); i.hasNext(); ) {
153 out.println(i.next());
154 }
155 }
156
157 public static void printHelp() {
158 out.println("Using Datalog:");
159 out.println();
160
161 out.println(" To specify a domain: \t<domain> <size> {<map-file-name>}");
162 out.println(" Example:\tV 1024");
163 out.println(" To specify a relation:\t<relation> (<attrib>:<domain>{,<attrib>:<domain>}*)");
164 out.println(" Example:\tR (v1:V, v2:V, h:H)");
165 out.println(" To specify a rule: \t<relation>(<var>{,<var>}*) :- {<relation>(<var>{,<var>}*),}*.");
166 out.println(" Example:\tR(a,b,c) :- R(b,a,c), Q(c).");
167 out.println(" Example:\tX(a,b,c) :- a!=b, b<c, Y(c).");
168 out.println(" To perform a query: \t<relation>(<var>{,<var>}*) {,<relation>(<var>{,<var>}*)}*?");
169 out.println(" Example:\tR(x,y,z), Q(z)?");
170 out.println();
171 out.println("Other commands:");
172 out.println();
173 out.println(" relations\t: list relations");
174 out.println(" rules \t: list rules");
175 out.println(" help \t: show this message");
176 out.println(" deleterule #{,#}*\t: delete rule(s)");
177 out.println(" save <relation>{,<relation>}\t: save relations");
178 out.println(" solve \t: solve current set of rules/relations");
179 out.println(" dumplog \t: dump the command log to a file");
180 out.println(" printlog \t: print the log to the screen");
181 out.println(" .include <file>\t: include (interpret) a file");
182 }
183
184 /***
185 * Invoke the interactive solver.
186 */
187 public void interactive() {
188 log = new LinkedList();
189 LineNumberReader lin = new LineNumberReader(new InputStreamReader(in));
190 MyReader in = new MyReader(lin);
191 for (;;) {
192 try {
193 out.print("> ");
194 String s = readLine(in);
195 if (s == null) break;
196 if (s.equalsIgnoreCase("exit") || s.equalsIgnoreCase("quit")) {
197 out.println("Exiting.");
198 return;
199 }
200 log.add(s);
201 if (s.equalsIgnoreCase("help")) {
202 printHelp();
203 continue;
204 }
205 if (s.equalsIgnoreCase("dumplog")) {
206 dumpLog();
207 out.println("Log dumped. ("+log.size()+" lines)");
208 continue;
209 }
210 if (s.equalsIgnoreCase("printlog")) {
211 printLog();
212 continue;
213 }
214 if (s.equalsIgnoreCase("solve")) {
215 changed = true;
216 solve();
217 continue;
218 }
219 if (s.equalsIgnoreCase("rules")) {
220 listRules();
221 continue;
222 }
223 if (s.equalsIgnoreCase("relations")) {
224 listRelations();
225 continue;
226 }
227 if (s.startsWith("deleterule")) {
228 if (s.length() <= 11) {
229 out.println("Usage: deleterule #{,#}");
230 } else {
231 List rules = parseRules(s.substring(11).trim());
232 if (rules != null && !rules.isEmpty()) {
233 solver.rules.removeAll(rules);
234 }
235 }
236 continue;
237 }
238 if (s.startsWith("save")) {
239 if (s.length() <= 5) {
240 out.println("Usage: save <relation>{,<relation>}");
241 } else {
242 List relations = parseRelations(s.substring(5).trim());
243 if (relations != null && !relations.isEmpty()) {
244 solver.relationsToDump.addAll(relations);
245 solve();
246 solver.relationsToDump.removeAll(relations);
247 }
248 }
249 continue;
250 }
251 Object result = parser.parseDatalogLine(s, in);
252 if (result != null) {
253 changed = true;
254 if (s.indexOf('?') >= 0 && result instanceof Collection) {
255
256 Collection queries = (Collection) result;
257 solve();
258 solver.rules.removeAll(queries);
259 for (Iterator i = queries.iterator(); i.hasNext(); ) {
260 InferenceRule ir = (InferenceRule) i.next();
261 solver.deleteRelation(ir.bottom.relation);
262 ir.bottom.relation.free();
263 ir.free();
264 }
265 }
266 }
267 } catch (NoSuchElementException x) {
268 out.println("Invalid command.");
269 log.remove(log.size()-1);
270 } catch (IllegalArgumentException x) {
271 out.println("Invalid command.");
272 log.remove(log.size()-1);
273 } catch (IOException x) {
274 out.println("IO Exception occurred: "+x);
275 }
276 }
277 }
278
279 /***
280 * Parse a list of relations.
281 *
282 * @param s string rep of list of relations
283 * @return list of relations
284 */
285 List parseRelations(String s) {
286 List relations = new LinkedList();
287 while (s.length() != 0) {
288 int i = s.indexOf(',');
289 String relationName;
290 if (i == -1) relationName = s;
291 else relationName = s.substring(0, i);
292 Relation r = solver.getRelation(relationName);
293 if (r == null) {
294 out.println("Unknown relation \""+relationName+"\"");
295 return null;
296 }
297 relations.add(r);
298 if (i == -1) break;
299 s = s.substring(i+1).trim();
300 }
301 return relations;
302 }
303
304 /***
305 * Parse a list of rules.
306 *
307 * @param s string rep of list of rules
308 * @return list of relations
309 */
310 List parseRules(String s) {
311 String ruleNum = null;
312 try {
313 List rules = new LinkedList();
314 for (;;) {
315 int i = s.indexOf(',');
316 if (i == -1) ruleNum = s;
317 else ruleNum = s.substring(0, i);
318 int k = Integer.parseInt(ruleNum);
319 if (k < 1 || k > solver.rules.size()) {
320 out.println("Rule number out of range: "+k);
321 return null;
322 }
323 rules.add(solver.rules.get(k-1));
324 if (i == -1) break;
325 s = s.substring(i+1).trim();
326 }
327 return rules;
328 } catch (NumberFormatException x) {
329 out.println("Not a number: \""+ruleNum+"\"");
330 }
331 return null;
332 }
333
334 /***
335 * List the relations the solver knows about.
336 */
337 void listRelations() {
338 out.println(solver.nameToRelation.keySet());
339 }
340
341 /***
342 * List the rules the solver knows about.
343 */
344 void listRules() {
345 int k = 0;
346 Iterator i = solver.rules.iterator();
347 if (!i.hasNext()) {
348 out.println("No rules defined.");
349 } else {
350 while (i.hasNext()) {
351 InferenceRule r = (InferenceRule) i.next();
352 ++k;
353 out.println(k+": "+r);
354 }
355 }
356 }
357
358 /***
359 * The set of relations that have been loaded, so we don't load them anymore.
360 */
361 Set loadedRelations = new HashSet();
362
363 /***
364 * Invoke the solver if we need to.
365 * Also loads relations that haven't been loaded, and saves results if necessary.
366 *
367 * @throws IOException
368 */
369 void solve() throws IOException {
370 if (changed) {
371 solver.splitRules();
372 if (solver.NOISY) solver.out.print("Initializing solver: ");
373 solver.initialize();
374 if (solver.NOISY) solver.out.println("done.");
375 if (!loadedRelations.containsAll(solver.relationsToLoad) ||
376 !loadedRelations.containsAll(solver.relationsToLoadTuples)) {
377 if (solver.NOISY) solver.out.print("Loading initial relations: ");
378 Set newRelationsToLoad = new HashSet(solver.relationsToLoad);
379 newRelationsToLoad.removeAll(loadedRelations);
380 long time = System.currentTimeMillis();
381 for (Iterator i = newRelationsToLoad.iterator(); i.hasNext();) {
382 Relation r = (Relation) i.next();
383 try {
384 r.load();
385 } catch (IOException x) {
386 out.println("WARNING: Cannot load bdd " + r + ": " + x.toString());
387 }
388 }
389 newRelationsToLoad = new HashSet(solver.relationsToLoadTuples);
390 newRelationsToLoad.removeAll(loadedRelations);
391 for (Iterator i = newRelationsToLoad.iterator(); i.hasNext();) {
392 Relation r = (Relation) i.next();
393 try {
394 r.loadTuples();
395 } catch (IOException x) {
396 out.println("WARNING: Cannot load tuples " + r + ": " + x.toString());
397 }
398 }
399 time = System.currentTimeMillis() - time;
400 if (solver.NOISY) solver.out.println("done. (" + time + " ms)");
401 loadedRelations.addAll(solver.relationsToLoad);
402 loadedRelations.addAll(solver.relationsToLoadTuples);
403 }
404 if (solver.relationsToDump.isEmpty() &&
405 solver.relationsToDumpTuples.isEmpty() &&
406 solver.relationsToPrintSize.isEmpty() &&
407 solver.relationsToPrintTuples.isEmpty() &&
408 solver.dotGraphsToDump.isEmpty()) {
409 solver.out.println("No relations marked as output! ");
410 if (IGNORE_OUTPUT)
411 out.println("(By default, the interactive driver ignores output keywords in the initial datalog.)");
412 solver.out.println("You need to specify at least one relation as one of the following:");
413 solver.out.println(" output");
414 solver.out.println(" outputtuples");
415 solver.out.println(" printsize");
416 solver.out.println(" printtuples");
417 solver.out.println("Alternatively, use a query like \"A(x,y)?\" rather than \"solve\".");
418 return;
419 }
420 if (solver.NOISY) solver.out.println("Stratifying: ");
421 long time = System.currentTimeMillis();
422 solver.stratify(solver.NOISY);
423 time = System.currentTimeMillis() - time;
424 if (solver.NOISY) solver.out.println("done. (" + time + " ms)");
425 if (solver.NOISY) solver.out.println("Solving: ");
426 time = System.currentTimeMillis();
427 solver.solve();
428 time = System.currentTimeMillis() - time;
429 if (solver.NOISY) solver.out.println("done. (" + time + " ms)");
430 long solveTime = time;
431 changed = false;
432 }
433 solver.saveResults();
434 }
435 }