1
2
3
4 package net.sf.bddbddb;
5
6 import java.util.ArrayList;
7 import java.util.Collection;
8 import java.util.Collections;
9 import java.util.HashMap;
10 import java.util.HashSet;
11 import java.util.Iterator;
12 import java.util.LinkedHashMap;
13 import java.util.LinkedList;
14 import java.util.List;
15 import java.util.Map;
16 import java.util.regex.Matcher;
17 import java.util.regex.Pattern;
18 import java.io.BufferedReader;
19 import java.io.File;
20 import java.io.FileReader;
21 import java.io.IOException;
22 import java.io.LineNumberReader;
23 import java.io.PrintStream;
24 import java.math.BigInteger;
25 import jwutil.collections.AppendIterator;
26 import jwutil.collections.Pair;
27 import jwutil.io.SystemProperties;
28 import jwutil.strings.MyStringTokenizer;
29 import jwutil.util.Assert;
30 import net.sf.bddbddb.Solver.MyReader;
31 import net.sf.bddbddb.dataflow.PartialOrder.BeforeConstraint;
32 import net.sf.bddbddb.dataflow.PartialOrder.InterleavedConstraint;
33
34 /***
35 * DatalogParser
36 *
37 * @author jwhaley
38 * @version $Id: DatalogParser.java 649 2006-09-16 05:51:04Z joewhaley $
39 */
40 public class DatalogParser {
41
42 /*** Solver object we are modifying. */
43 Solver solver;
44
45 /*** Trace flag. */
46 boolean TRACE = SystemProperties.getProperty("traceparse") != null;
47 boolean STRICT_DECLARATIONS = !SystemProperties.getProperty("strict", "no").equals("no");
48 boolean ALLOW_SINGLE_USE = !SystemProperties.getProperty("singleignore", "no").equals("no");
49
50 /*** Trace output stream. */
51 public PrintStream out;
52 public PrintStream err;
53
54 /***
55 * Construct a new Datalog parser with the given solver.
56 *
57 * @param solver add rules, relations, etc. to this solver
58 */
59 public DatalogParser(Solver solver) {
60 this.solver = solver;
61 this.out = solver.out;
62 this.err = solver.err;
63 }
64
65 /***
66 * Utility function to read a line from the given reader.
67 * Allows line wrapping using backslashes, among other things.
68 *
69 * @param in input reader
70 * @return line
71 * @throws IOException
72 */
73 static String readLine(MyReader in) throws IOException {
74 String s = in.readLine();
75 if (s == null) return null;
76 s = s.trim();
77 while (s.endsWith("//")) {
78 String s2 = in.readLine();
79 if (s2 == null) break;
80 s2 = s2.trim();
81 s = s.substring(0, s.length() - 1) + s2;
82 }
83 return s;
84 }
85
86 /***
87 * Get the next token, skipping over spaces.
88 *
89 * @param st string tokenizer
90 * @return next non-space token
91 */
92 static String nextToken(MyStringTokenizer st) {
93 String s;
94 do {
95 s = st.nextToken();
96 } while (s.equals(" ") || s.equals("\t"));
97 return s;
98 }
99
100 /***
101 * Read and parse a Datalog program.
102 *
103 * @param inputFilename name of file to read
104 * @throws IOException
105 */
106 public void readDatalogProgram(String inputFilename) throws IOException {
107 MyReader in = null;
108 try {
109 in = new MyReader(new LineNumberReader(new FileReader(inputFilename)));
110 readDatalogProgram(in);
111 } finally {
112 if (in != null) try { in.close(); } catch (IOException _) { }
113 }
114 }
115
116 /***
117 * Read and parse a Datalog program.
118 *
119 * @param in input reader
120 * @throws IOException
121 */
122 public void readDatalogProgram(MyReader in) throws IOException {
123 for (;;) {
124 String s = readLine(in);
125 if (s == null) break;
126 parseDatalogLine(s, in);
127 }
128 }
129
130 /***
131 * Parse a line from a Datalog program.
132 *
133 * @param s line to parse
134 * @param in input reader
135 * @return the rule, relation, domain, or list of rules we parsed, or null
136 * @throws IOException
137 */
138 Object parseDatalogLine(String s, MyReader in) throws IOException {
139 if (s.length() == 0) return null;
140 if (s.startsWith("#")) return null;
141 int lineNum = in.getLineNumber();
142 if (s.startsWith(".")) {
143
144 parseDirective(in, lineNum, s);
145 return null;
146 }
147 MyStringTokenizer st = new MyStringTokenizer(s);
148 if (st.hasMoreTokens()) {
149 st.nextToken();
150 if (st.hasMoreTokens()) {
151 String num = st.nextToken();
152 boolean isNumber;
153 try {
154 new BigInteger(num);
155 isNumber = true;
156 } catch (NumberFormatException x) {
157 isNumber = false;
158 }
159 if (isNumber) {
160
161 Domain fd = parseDomain(lineNum, s);
162 if (TRACE) out.println("Parsed field domain " + fd + " size " + fd.size);
163 if (solver.nameToDomain.containsKey(fd.name)) {
164 err.println("Error, field domain " + fd.name + " redefined on line " + in.getLineNumber() + ", ignoring.");
165 } else {
166 solver.nameToDomain.put(fd.name, fd);
167 }
168 return fd;
169 }
170 }
171 }
172 int dotIndex = s.indexOf('.');
173 int braceIndex = s.indexOf('{');
174 int qIndex = s.indexOf('?');
175 if (dotIndex > 0 && (braceIndex == -1 || dotIndex < braceIndex)) {
176
177 try {
178 InferenceRule ir = parseRule(lineNum, s);
179 if (TRACE) out.println("Parsed rule " + ir);
180 solver.rules.add(ir);
181 return Collections.singletonList(ir);
182 } finally {
183 deleteUndeclaredRelations();
184 }
185 } else if (qIndex > 0 && (braceIndex == -1 || qIndex < braceIndex)) {
186 try {
187
188 List
189 if (ir != null) {
190 if (TRACE) out.println("Parsed query " + ir);
191 solver.rules.addAll(ir);
192 }
193 return ir;
194 } finally {
195 deleteUndeclaredRelations();
196 }
197 } else {
198
199 Relation r = parseRelation(lineNum, s);
200 if (TRACE && r != null) out.println("Parsed relation " + r);
201 return r;
202 }
203 }
204
205 /***
206 * Output a parse error at the given location.
207 *
208 * @param linenum line number of error
209 * @param colnum column number of error
210 * @param line text of line containing error
211 * @param msg error message
212 */
213 void outputError(int linenum, int colnum, String line, String msg) {
214 err.println("Error on line " + linenum + ":");
215 err.println(line);
216 while (--colnum >= 0)
217 err.print(' ');
218 err.println('^');
219 err.println(msg);
220 }
221
222 /***
223 * Parse a directive.
224 *
225 * @param in input reader
226 * @param lineNum current line number, for debugging purposes
227 * @param s string containing directive to parse
228 * @throws IOException
229 */
230 void parseDirective(MyReader in, int lineNum, String s) throws IOException {
231 if (s.startsWith(".include")) {
232 int index = ".include".length() + 1;
233 String fileName = s.substring(index).trim();
234 if (fileName.startsWith("\"")) {
235 if (!fileName.endsWith("\"")) {
236 outputError(lineNum, index, s,
237 "Unmatched quotes");
238 throw new IllegalArgumentException();
239 }
240 fileName = fileName.substring(1, fileName.length() - 1);
241 }
242 if (!fileName.startsWith("/")) {
243 String[] dirs = solver.includedirs.split(SystemProperties.getProperty("path.separator"));
244 for (int i=0; i<dirs.length; i++) {
245 if ((new File(dirs[i],fileName)).exists()) {
246 fileName = dirs[i]+SystemProperties.getProperty("file.separator")+fileName;
247 break;
248 }
249 }
250 }
251 in.registerReader(new LineNumberReader(new FileReader(fileName)));
252 } else if (s.startsWith(".split_all_rules")) {
253 boolean b = true;
254 int index = ".split_all_rules".length() + 1;
255 if (s.length() > index) {
256 String option = s.substring(index).trim();
257 b = !option.equals("false") && !option.equals("no");
258 }
259 solver.SPLIT_ALL_RULES = b;
260 } else if (s.startsWith(".report_stats")) {
261 boolean b = true;
262 int index = ".report_stats".length() + 1;
263 if (s.length() > index) {
264 String option = s.substring(index).trim();
265 b = !option.equals("false") && !option.equals("no");
266 }
267 solver.REPORT_STATS = b;
268 } else if (s.startsWith(".noisy")) {
269 boolean b = true;
270 int index = ".noisy".length() + 1;
271 if (s.length() > index) {
272 String option = s.substring(index).trim();
273 b = !option.equals("false") && !option.equals("no");
274 }
275 solver.NOISY = b;
276 } else if (s.startsWith(".strict")) {
277 boolean b = true;
278 int index = ".strict".length() + 1;
279 if (s.length() > index) {
280 String option = s.substring(index).trim();
281 b = !option.equals("false") && !option.equals("no");
282 }
283 STRICT_DECLARATIONS = b;
284 } else if (s.startsWith(".singleignore")) {
285 boolean b = true;
286 int index = ".singleignore".length() + 1;
287 if (s.length() > index) {
288 String option = s.substring(index).trim();
289 b = !option.equals("false") && !option.equals("no");
290 }
291 ALLOW_SINGLE_USE = b;
292 }
293 else if (s.startsWith(".trace")) {
294 boolean b = true;
295 int index = ".trace".length() + 1;
296 if (s.length() > index) {
297 String option = s.substring(index).trim();
298 b = !option.equals("false") && !option.equals("no");
299 }
300 solver.TRACE = TRACE = b;
301 } else if (s.startsWith(".bddvarorder")) {
302 if (SystemProperties.getProperty("bddvarorder") == null) {
303 int index = ".bddvarorder".length() + 1;
304 String varOrder = s.substring(index).trim();
305 if (solver instanceof BDDSolver) {
306 ((BDDSolver) solver).VARORDER = varOrder;
307 } else {
308 err.println("Ignoring .bddvarorder "+varOrder);
309 }
310 }
311 } else if (s.startsWith(".bddnodes")) {
312 if (SystemProperties.getProperty("bddnodes") == null) {
313 int index = ".bddnodes".length() + 1;
314 int n = Integer.parseInt(s.substring(index).trim());
315 if (solver instanceof BDDSolver) {
316 ((BDDSolver) solver).BDDNODES = n;
317 } else {
318 err.println("Ignoring .bddnodes "+n);
319 }
320 }
321 } else if (s.startsWith(".bddcache")) {
322 if (SystemProperties.getProperty("bddcache") == null) {
323 int index = ".bddcache".length() + 1;
324 int n = Integer.parseInt(s.substring(index).trim());
325 if (solver instanceof BDDSolver) {
326 ((BDDSolver) solver).BDDCACHE = n;
327 } else {
328 err.println("Ignoring .bddcache "+n);
329 }
330 }
331 } else if (s.startsWith(".bddminfree")) {
332 if (SystemProperties.getProperty("bddminfree") == null) {
333 int index = ".bddminfree".length() + 1;
334 double n = Double.parseDouble(s.substring(index).trim());
335 if (solver instanceof BDDSolver) {
336 ((BDDSolver) solver).BDDMINFREE = n;
337 } else {
338 err.println("Ignoring .bddminfree "+n);
339 }
340 }
341 } else if (s.startsWith(".findbestorder")) {
342 int index = ".findbestorder".length() + 1;
343 String val = "";
344 if (s.length() > index) val = s.substring(index).trim();
345 System.setProperty("findbestorder", val);
346 } else if (s.startsWith(".incremental")) {
347 int index = ".incremental".length() + 1;
348 String val = "";
349 if (s.length() > index) val = s.substring(index).trim();
350 System.setProperty("incremental", val);
351 } else if (s.startsWith(".dot")) {
352 int index = ".dot".length() + 1;
353 String dotSpec = "";
354 if (s.length() > index) dotSpec = s.substring(index).trim();
355 Dot dot = new Dot();
356 LineNumberReader lnr = new LineNumberReader(new FileReader(solver.basedir + dotSpec));
357 if (TRACE) out.println("Parsing dot " + dotSpec);
358 dot.parseInput(solver, lnr);
359 if (TRACE) out.println("Done parsing dot " + dotSpec);
360 lnr.close();
361 solver.dotGraphsToDump.add(dot);
362 } else if (s.startsWith(".basedir")) {
363 if (SystemProperties.getProperty("basedir") == null) {
364 int index = ".basedir".length() + 1;
365 String dirName = s.substring(index).trim();
366 if (dirName.startsWith("\"") && dirName.endsWith("\"")) {
367 dirName = dirName.substring(1, dirName.length() - 1);
368 }
369 solver.basedir += dirName;
370 String sep = SystemProperties.getProperty("file.separator");
371 if (!solver.basedir.endsWith(sep) && !solver.basedir.endsWith("/")) {
372 solver.basedir += sep;
373 }
374 if (TRACE) out.println("Base directory is now \"" + solver.basedir + "\"");
375 Assert._assert(solver.includedirs != null);
376 solver.includedirs += SystemProperties.getProperty("path.separator") + solver.basedir;
377 }
378 } else {
379 outputError(lineNum, 0, s,
380 "Unknown directive \"" + s + "\"");
381 throw new IllegalArgumentException();
382 }
383 }
384
385 /***
386 * Parse a domain declaration.
387 *
388 * @param lineNum current line number for outputting error messages
389 * @param s string containing relation declaration
390 * @return new domain
391 */
392 Domain parseDomain(int lineNum, String s) {
393 MyStringTokenizer st = new MyStringTokenizer(s);
394 String name = nextToken(st);
395 String num = nextToken(st);
396 BigInteger size;
397 try {
398 size = new BigInteger(num);
399 } catch (NumberFormatException x) {
400 outputError(lineNum, st.getPosition(), s,
401 "Expected a number, got \"" + num + "\"");
402 throw new IllegalArgumentException();
403 }
404 Domain fd = new Domain(name, size);
405 if (st.hasMoreTokens()) {
406 String mapName = nextToken(st);
407 BufferedReader dis = null;
408 try {
409 dis = new BufferedReader(new FileReader(solver.basedir + mapName));
410 fd.loadMap(dis);
411 } catch (IOException x) {
412 err.println("WARNING: Cannot load mapfile \"" + solver.basedir + mapName + "\", skipping.");
413 } finally {
414 if (dis != null) try { dis.close(); } catch (IOException x) { }
415 }
416 }
417 return fd;
418 }
419
420 static final char[] badchars = new char[] { '!', '=', ':', '-', '<', '>', '(', ')', ',', ' ', '\t', '\f' };
421
422 /***
423 * Parse a relation declaration.
424 *
425 * @param lineNum current line number for outputting error messages
426 * @param s string containing relation declaration
427 * @return new relation, or null if the relation was already defined
428 */
429 Relation parseRelation(int lineNum, String s) {
430 MyStringTokenizer st = new MyStringTokenizer(s, " \t(:,)", true);
431 String name = nextToken(st);
432 for (int i = 0; i < badchars.length; ++i) {
433 if (name.indexOf(badchars[i]) >= 0) {
434 outputError(lineNum, st.getPosition(), s,
435 "Relation name cannot contain '"+badchars[i]+"'");
436 throw new IllegalArgumentException();
437 }
438 }
439 String openParen = nextToken(st);
440 if (!openParen.equals("(")) {
441 outputError(lineNum, st.getPosition(), s,
442 "Expected \"(\", got \"" + openParen + "\"");
443 throw new IllegalArgumentException();
444 }
445 List attributes = new LinkedList();
446 for (;;) {
447 String fName = nextToken(st);
448 String colon = nextToken(st);
449 if (!colon.equals(":")) {
450 outputError(lineNum, st.getPosition(), s,
451 "Expected \":\", got \"" + colon + "\"");
452 throw new IllegalArgumentException();
453 }
454 String fdName = nextToken(st);
455 int numIndex = fdName.length() - 1;
456 for (;;) {
457 char c = fdName.charAt(numIndex);
458 if (c < '0' || c > '9') break;
459 --numIndex;
460 if (numIndex < 0) {
461 outputError(lineNum, st.getPosition(), s,
462 "Expected field domain name, got \"" + fdName + "\"");
463 throw new IllegalArgumentException();
464 }
465 }
466 ++numIndex;
467 int fdNum = -1;
468 if (numIndex < fdName.length()) {
469 String number = fdName.substring(numIndex);
470 try {
471 fdNum = Integer.parseInt(number);
472 } catch (NumberFormatException x) {
473 outputError(lineNum, st.getPosition(), s,
474 "Cannot parse field domain number \"" + number + "\"");
475 throw new IllegalArgumentException();
476 }
477 fdName = fdName.substring(0, numIndex);
478 }
479 Domain fd = solver.getDomain(fdName);
480 if (fd == null) {
481 outputError(lineNum, st.getPosition(), s,
482 "Unknown field domain " + fdName);
483 throw new IllegalArgumentException();
484 }
485 String option;
486 if (fdNum != -1) option = fdName + fdNum;
487 else option = "";
488 attributes.add(new Attribute(fName, fd, option));
489 String comma = nextToken(st);
490 if (comma.equals(")")) break;
491 if (!comma.equals(",")) {
492 outputError(lineNum, st.getPosition(), s,
493 "Expected \",\" or \")\", got \"" + comma + "\"");
494 throw new IllegalArgumentException();
495 }
496 }
497 if (solver.nameToRelation.containsKey(name)) {
498 outputError(lineNum, st.getPosition(), s,"Relation " + name + " redefined");
499 throw new IllegalArgumentException();
500
501 }
502 Relation r = solver.createRelation(name, attributes);
503 Pattern constraintPattern = Pattern.compile("(//w+)([=<])(//w+)");
504 while (st.hasMoreTokens()) {
505 String option = nextToken(st);
506 Matcher constraintMatcher = constraintPattern.matcher(option);
507 if (option.equals("output")) {
508 solver.relationsToDump.add(r);
509 } else if (option.equals("outputtuples")) {
510 solver.relationsToDumpTuples.add(r);
511 } else if (option.equals("input")) {
512 solver.relationsToLoad.add(r);
513 } else if (option.equals("inputtuples")) {
514 solver.relationsToLoadTuples.add(r);
515 } else if (option.equals("printtuples")) {
516 solver.relationsToPrintTuples.add(r);
517 } else if (option.equals("printsize")) {
518 solver.relationsToPrintSize.add(r);
519 } else if (option.startsWith("pri")) {
520 String num = option.substring(4);
521 int pri = Integer.parseInt(num);
522 r.priority = pri;
523 } else if (option.equals("{")) {
524 String s2 = nextToken(st);
525 StringBuffer sb = new StringBuffer();
526 while (!s2.equals("}")) {
527 sb.append(' ');
528 sb.append(s2);
529 if (!st.hasMoreTokens()) {
530 outputError(lineNum, st.getPosition(), s,
531 "Expected \"}\" to terminate code block");
532 throw new IllegalArgumentException();
533 }
534 s2 = nextToken(st);
535 }
536 CodeFragment f = new CodeFragment(sb.toString(), r);
537 r.onUpdate.add(f);
538 } else if (constraintMatcher.matches()) {
539 parseAndAddConstraint(r, constraintMatcher);
540 } else {
541 outputError(lineNum, st.getPosition(), s,
542 "Unexpected option '" + option + "'");
543 solver.deleteRelation(r);
544 throw new IllegalArgumentException();
545 }
546 }
547 if (!r.constraints.isEmpty()) {
548 r.constraints.satisfy();
549 }
550 return r;
551 }
552
553 /***
554 * Parse and add an attribute constraint.
555 *
556 * @param r relation to add constraint for
557 * @param m constraint pattern matcher
558 */
559 public void parseAndAddConstraint(Relation r, Matcher m) {
560 if (m.matches()) {
561 String leftAttr = m.group(1);
562 String type = m.group(2);
563 String rightAttr = m.group(3);
564 Attribute left = null;
565 Attribute right = null;
566 for (Iterator it = r.getAttributes().iterator(); it.hasNext();) {
567 Attribute a = (Attribute) it.next();
568 if (a.attributeName.equals(leftAttr)) left = a;
569 if (a.attributeName.equals(rightAttr)) right = a;
570 }
571 if (left == null) {
572 out.println("Specified Attribute not found: " + leftAttr);
573 throw new IllegalArgumentException();
574 } else if (right == null) {
575 out.println("Specified Attribute not found: " + rightAttr);
576 throw new IllegalArgumentException();
577 }
578
579 if (type.equals("=")) r.constraints.addInterleavedConstraint(new InterleavedConstraint(r,left,r,right,10));
580 else if (type.equals("<")) r.constraints.addBeforeConstraint(new BeforeConstraint(r,left,r,right,10));
581 if (TRACE) out.println("parsed constraint: " + leftAttr + " " + type + " " + rightAttr);
582 } else {
583
584 }
585 }
586
587 /***
588 * Parse an inference rule.
589 *
590 * @param lineNum current line number for outputting error messages
591 * @param s string containing rule to parse
592 * @return new inference rule
593 */
594 InferenceRule parseRule(int lineNum, String s) {
595 MyStringTokenizer st = new MyStringTokenizer(s, " \t(,/).=!<>", true);
596 Map
597 undeclaredRelations.clear();
598 RuleTerm bottom = parseRuleTerm(lineNum, s, nameToVar, st);
599 String sep = nextToken(st);
600 List
601 if (!sep.equals(".")) {
602 if (!sep.equals(":-")) {
603 outputError(lineNum, st.getPosition(), s,
604 "Expected \":-\", got \"" + sep + "\"");
605 throw new IllegalArgumentException();
606 }
607 for (;;) {
608 RuleTerm rt = parseRuleTerm(lineNum, s, nameToVar, st);
609 if (rt == null) break;
610 terms.add(rt);
611 sep = nextToken(st);
612 if (sep.equals(".")) break;
613 if (!sep.equals(",")) {
614 outputError(lineNum, st.getPosition(), s,
615 "Expected \".\" or \",\", got \"" + sep + "\"");
616 throw new IllegalArgumentException();
617 }
618 }
619 }
620 handleUndeclaredRelations(lineNum, s, nameToVar, terms, bottom);
621 InferenceRule ir = solver.createInferenceRule(terms, bottom);
622 ir = parseRuleOptions(lineNum, s, ir, st);
623 Variable v = ir.checkUnnecessaryVariables();
624 if (!ALLOW_SINGLE_USE && v != null) {
625 outputError(lineNum, st.getPosition(), s,
626 "Variable "+v+" was only used once! Use '_' instead.");
627 throw new IllegalArgumentException();
628 }
629 return ir;
630 }
631
632 /***
633 * Finish the declaration of undeclared relations.
634 */
635 void handleUndeclaredRelations(int lineNum, String s, Map nameToVar,
636 List terms, RuleTerm bottom) {
637 for (;;) {
638 boolean change = false;
639 for (Iterator i = undeclaredRelations.iterator(); i.hasNext(); ) {
640 Relation r = (Relation) i.next();
641 boolean any = false;
642 for (Iterator j = r.attributes.iterator(); j.hasNext(); ) {
643 Attribute a = (Attribute) j.next();
644 if (a.attributeDomain == null) {
645
646 any = true;
647 String name = a.attributeName;
648 Variable v = (Variable) nameToVar.get(name);
649 if (v == null) {
650 outputError(lineNum, 0, s,
651 "Cannot find variable "+name);
652 throw new IllegalArgumentException();
653 }
654 if (v.domain != null) {
655 a.attributeDomain = v.domain;
656 change = true;
657 }
658 }
659 }
660 if (!any) {
661 if (solver.NOISY) out.println("Implicitly defining relation "+r.verboseToString());
662 i.remove();
663
664 Iterator j = terms.iterator();
665 if (bottom != null)
666 j = new AppendIterator(j, Collections.singleton(bottom).iterator());
667 while (j.hasNext()) {
668 RuleTerm rt = (RuleTerm) j.next();
669 if (rt.relation != r) continue;
670 for (int k = 0; k < r.numberOfAttributes(); ++k) {
671 Variable v = rt.getVariable(k);
672 if (v.domain != null) continue;
673 Attribute a = r.getAttribute(k);
674 v.domain = a.attributeDomain;
675 change = true;
676 }
677 }
678 }
679 }
680 if (!change) break;
681 }
682 if (!undeclaredRelations.isEmpty()) {
683 outputError(lineNum, 0, s,
684 "Cannot infer attributes for undeclared relations "+undeclaredRelations);
685 throw new IllegalArgumentException();
686 }
687 }
688
689 void deleteUndeclaredRelations() {
690 for (Iterator i = undeclaredRelations.iterator(); i.hasNext(); ) {
691 Relation r = (Relation) i.next();
692 solver.deleteRelation(r);
693 i.remove();
694 }
695 }
696
697 /***
698 * Parse the options for an inference rule.
699 *
700 * @param lineNum current line number for outputting error messages
701 * @param s current line for outputting error messages
702 * @param ir inference rule to parse options for
703 * @param st string tokenizer containing options to parse
704 * @return the resulting rule
705 */
706 InferenceRule parseRuleOptions(int lineNum, String s, InferenceRule ir, MyStringTokenizer st) {
707 while (st.hasMoreTokens()) {
708 String option = nextToken(st);
709 if (option.equals("split")) {
710 if (!solver.SPLIT_NO_RULES) {
711 if (TRACE) out.println("Splitting rule " + ir);
712 ir.split = true;
713 }
714 } else if (option.equals("number")) {
715 if (TRACE) out.println("Rule " + ir + " defines a numbering");
716 ir = solver.createNumberingRule(ir);
717 } else if (option.equals("single")) {
718 if (TRACE) out.println("Rule " + ir + " only adds a single satisfying assignment");
719 ir.single = true;
720 } else if (option.equals("cacheafterrename")) {
721 BDDInferenceRule r = (BDDInferenceRule) ir;
722 r.cache_before_rename = false;
723 } else if (option.equals("findbestorder")) {
724 BDDInferenceRule r = (BDDInferenceRule) ir;
725 r.find_best_order = true;
726 } else if (option.equals("trace")) {
727 BDDInferenceRule r = (BDDInferenceRule) ir;
728 r.TRACE = true;
729 } else if (option.equals("tracefull")) {
730 BDDInferenceRule r = (BDDInferenceRule) ir;
731 r.TRACE = true;
732 r.TRACE_FULL = true;
733 } else if (option.equals("pri")) {
734 String num = nextToken(st);
735 if (num.equals("=")) num = nextToken(st);
736 int pri = Integer.parseInt(num);
737 ir.priority = pri;
738 } else if (option.equals("pre") || option.equals("post") || option.equals("{")) {
739 StringBuffer sb = new StringBuffer();
740 String s2 = nextToken(st);
741 int type = 2;
742 if (!option.equals("{")) {
743 if (option.equals("pre")) type = 1;
744 if (!s2.equals("{")) {
745 outputError(lineNum, st.getPosition(), s,
746 "Expected \"{\", but found \""+s2+"\"");
747 throw new IllegalArgumentException();
748 }
749 s2 = nextToken(st);
750 }
751 while (!s2.equals("}")) {
752 sb.append(' ');
753 sb.append(s2);
754 if (!st.hasMoreTokens()) {
755 outputError(lineNum, st.getPosition(), s,
756 "Expected \"}\" to terminate code block");
757 throw new IllegalArgumentException();
758 }
759 s2 = nextToken(st);
760 }
761 CodeFragment f = new CodeFragment(sb.toString(), ir);
762 if (type == 1) ir.preCode.add(f);
763 else ir.postCode.add(f);
764 } else if (option.equals("modifies")) {
765 String relationName = nextToken(st);
766 if (relationName.equals("(")) {
767 for (;;) {
768 relationName = nextToken(st);
769 if (relationName.equals(",")) continue;
770 if (relationName.equals(")")) break;
771 Relation r = solver.getRelation(relationName);
772 if (r == null) {
773 outputError(lineNum, st.getPosition(), s,
774 "Unknown relation \""+relationName+"\"");
775 throw new IllegalArgumentException();
776 }
777 ir.extraDefines.add(r);
778 }
779 } else {
780 Relation r = solver.getRelation(relationName);
781 if (r == null) {
782 outputError(lineNum, st.getPosition(), s,
783 "Unknown relation \""+relationName+"\"");
784 throw new IllegalArgumentException();
785 }
786 ir.extraDefines.add(r);
787 }
788 } else {
789
790 outputError(lineNum, st.getPosition(), s,
791 "Unknown rule option \"" + option + "\"");
792 throw new IllegalArgumentException();
793 }
794 }
795 if (hasDuplicateVars && !(ir instanceof NumberingRule)) {
796 outputError(lineNum, st.getPosition(), s,
797 "Variable repeated multiple times in a single term");
798 throw new IllegalArgumentException();
799 }
800 hasDuplicateVars = false;
801 return ir;
802 }
803
804 /***
805 * Flag that is set if a rule term has repeated variables.
806 */
807 boolean hasDuplicateVars;
808
809 /***
810 * Temporary collection to hold undeclared relations.
811 */
812 Collection undeclaredRelations = new LinkedList();
813
814 /***
815 * Parse a term of an inference rule.
816 *
817 * @param lineNum current line number for outputting error messages
818 * @param s current line for outputting error messages
819 * @param nameToVar map from variable names to variables
820 * @param st string tokenizer containing rule term to parse
821 * @return rule term, or null if string is "?"
822 */
823 RuleTerm parseRuleTerm(int lineNum, String s, Map
824 boolean negated = false;
825 String relationName = nextToken(st);
826 if (relationName.equals("?")) {
827 return null;
828 }
829 if (relationName.equals("!")) {
830 negated = true;
831 relationName = nextToken(st);
832 }
833 String openParen = nextToken(st);
834 boolean flip = false;
835 boolean less = false;
836 boolean greater = false;
837 if (openParen.equals("!")) {
838 flip = true;
839 openParen = nextToken(st);
840 } else if (openParen.equals("<")) {
841 less = true;
842 openParen = nextToken(st);
843 } else if (openParen.equals(">")) {
844 greater = true;
845 openParen = nextToken(st);
846 }
847 if (openParen.equals("=") || less || greater) {
848 if (negated) {
849 outputError(lineNum, st.getPosition(), s,
850 "Unexpected \"!\"");
851 throw new IllegalArgumentException();
852 }
853
854 boolean equals = openParen.equals("=");
855 String varName1 = relationName;
856 String varName2 = equals ? nextToken(st) : openParen;
857 Variable var1, var2;
858 var1 = (Variable) nameToVar.get(varName1);
859 Relation r;
860 if (equals && varName2.equals(">")) {
861 if (negated || less || greater) {
862 outputError(lineNum, st.getPosition(), s,
863 "Unexpected \"!\", \"<\", or \">\" with \"=>\"");
864 throw new IllegalArgumentException();
865 }
866
867 varName2 = nextToken(st);
868 var2 = (Variable) nameToVar.get(varName2);
869 if (var1 == null || var2 == null) {
870 outputError(lineNum, st.getPosition(), s,
871 "Cannot use \"=>\" on unbound variables.");
872 throw new IllegalArgumentException();
873 }
874 r = solver.getMapRelation(var1.domain, var2.domain);
875 } else {
876 var2 = (Variable) nameToVar.get(varName2);
877 if (var1 == null) {
878 if (var2 == null) {
879 outputError(lineNum, st.getPosition(), s,
880 "Cannot use \"=\", \"!=\", \"<\", \"<=\", \">\", \">=\", on two unbound variables.");
881 throw new IllegalArgumentException();
882 }
883 var1 = parseVariable(var2.domain, nameToVar, varName1);
884 } else {
885 if (var2 == null) {
886 var2 = parseVariable(var1.domain, nameToVar, varName2);
887 }
888 }
889 if (var1.domain == null) var1.domain = var2.domain;
890 if (var2.domain == null) var2.domain = var1.domain;
891 if (var1.domain == null && var2.domain == null) {
892 outputError(lineNum, st.getPosition(), s,
893 "Cannot infer domain for variables "+var1+" and "+var2+" used in comparison.");
894 throw new IllegalArgumentException();
895 }
896 if (less) {
897 r = equals ? solver.getLessThanOrEqualRelation(var1.domain, var2.domain) : solver.getLessThanRelation(var1.domain, var2.domain);
898 } else if (greater) {
899 r = equals ? solver.getGreaterThanOrEqualRelation(var1.domain, var2.domain) : solver.getGreaterThanRelation(var1.domain, var2.domain);
900 } else {
901 r = flip ? solver.getNotEquivalenceRelation(var1.domain, var2.domain) : solver.getEquivalenceRelation(var1.domain, var2.domain);
902 }
903 }
904 List vars = new Pair(var1, var2);
905 RuleTerm rt = new RuleTerm(r, vars);
906 return rt;
907 } else if (!openParen.equals("(")) {
908 outputError(lineNum, st.getPosition(), s,
909 "Expected \"(\" or \"=\", got \"" + openParen + "\"");
910 throw new IllegalArgumentException();
911 }
912 if (flip) {
913 outputError(lineNum, st.getPosition(), s,
914 "Unexpected \"!\"");
915 throw new IllegalArgumentException();
916 }
917 Relation r = solver.getRelation(relationName);
918 if (STRICT_DECLARATIONS && r == null) {
919 outputError(lineNum, st.getPosition(), s,
920 "Unknown relation " + relationName);
921 throw new IllegalArgumentException();
922 }
923 if (negated && r != null) r = r.makeNegated(solver);
924 List
925 for (;;) {
926 if (r != null && r.attributes.size() <= vars.size()) {
927 outputError(lineNum, st.getPosition(), s,
928 "Too many fields for " + r);
929 throw new IllegalArgumentException();
930 }
931 Attribute a = null;
932 Domain fd = null;
933 if (r != null) {
934 a = (Attribute) r.attributes.get(vars.size());
935 fd = a.attributeDomain;
936 }
937 String varName = nextToken(st);
938 Variable var = parseVariable(fd, nameToVar, varName);
939 if (vars.contains(var) && !varName.equals("*")) {
940 hasDuplicateVars = true;
941 }
942 vars.add(var);
943 if (var.domain == null) var.domain = fd;
944 else if (fd != null && var.domain != fd) {
945 outputError(lineNum, st.getPosition(), s,
946 "Variable " + var + " used as both " + var.domain + " and " + fd);
947 throw new IllegalArgumentException();
948 }
949 String sep = nextToken(st);
950 if (sep.equals(")")) break;
951 if (!sep.equals(",")) {
952 outputError(lineNum, st.getPosition(), s,
953 "Expected ',' or ')', got '" + sep + "'");
954 throw new IllegalArgumentException();
955 }
956 }
957 if (r != null && r.attributes.size() != vars.size()) {
958 outputError(lineNum, st.getPosition(), s,
959 "Wrong number of vars in rule term for " + relationName +
960 " (expected "+r.attributes.size()+", found "+vars.size()+")");
961 throw new IllegalArgumentException();
962 }
963 if (r == null) {
964
965 List
966 for (Iterator i = vars.iterator(); i.hasNext(); ) {
967 Variable v = (Variable) i.next();
968 if (v instanceof Constant || "_".equals(v.name)) {
969 outputError(lineNum, st.getPosition(), s,
970 "Cannot infer attribute for '"+v.name+"' in undeclared relation "+relationName);
971 throw new IllegalArgumentException();
972 }
973 Attribute a = new Attribute(v.name, v.domain, null);
974 attribs.add(a);
975 }
976 r = solver.createRelation(relationName, attribs);
977 undeclaredRelations.add(r);
978 }
979 RuleTerm rt = new RuleTerm(r, vars);
980 return rt;
981 }
982
983 /***
984 * Parse a variable or a constant.
985 *
986 * @param fd domain of variable/constant
987 * @param nameToVar map from names to variables for this rule
988 * @param varName name of variable/constant
989 * @return variable/constant
990 */
991 Variable parseVariable(Domain fd, Map nameToVar, String varName) {
992 char firstChar = varName.charAt(0);
993 Variable var;
994 if (firstChar >= '0' && firstChar <= '9') {
995 var = new Constant(Long.parseLong(varName));
996 } else if (firstChar == '"') {
997 if (fd == null) {
998 throw new IllegalArgumentException("Cannot use quoted constant "+varName+" in undeclared relation");
999 }
1000 String namedConstant = varName.substring(1, varName.length() - 1);
1001 var = new Constant(fd.namedConstant(namedConstant));
1002 } else if (varName.equals("*")) {
1003 var = new Universe(fd);
1004 } else if (!varName.equals("_")) {
1005 var = (Variable) nameToVar.get(varName);
1006 if (var == null) nameToVar.put(varName, var = new Variable(varName));
1007 } else {
1008 var = new Variable();
1009 }
1010 if (var.domain == null) var.domain = fd;
1011 return var;
1012 }
1013
1014 /***
1015 * Parse a query. A query is a statement that ends with '?'.
1016 *
1017 * @param lineNum current line number, for outputting error messages
1018 * @param s line to parse
1019 * @return list of inference rules implementing the query.
1020 */
1021 List
1022 MyStringTokenizer st = new MyStringTokenizer(s, " \t(,/).=~!?<>", true);
1023 Map
1024
1025 undeclaredRelations.clear();
1026
1027 if (s.indexOf(":-") > 0) {
1028 RuleTerm rt = parseRuleTerm(lineNum, s, nameToVar, st);
1029 String sep = nextToken(st);
1030 if (!sep.equals(":-")) {
1031 outputError(lineNum, st.getPosition(), s, "Expected \":-\", got \"" + sep + "\"");
1032 throw new IllegalArgumentException();
1033 }
1034 List
1035 for (;;) {
1036 RuleTerm rt2 = parseRuleTerm(lineNum, s, nameToVar, st);
1037 if (rt2 == null) break;
1038 extras.add(rt2);
1039 String sep2 = nextToken(st);
1040 if (sep2.equals("?")) break;
1041 if (!sep2.equals(",")) {
1042 outputError(lineNum, st.getPosition(), s, "Expected \",\", got \"" + sep2 + "\"");
1043 throw new IllegalArgumentException();
1044 }
1045 }
1046 boolean single = false;
1047 while (st.hasMoreTokens()) {
1048 String option = nextToken(st);
1049 if (option.equals("single")) {
1050 single = true;
1051 } else {
1052 outputError(lineNum, st.getPosition(), s, "Unknown query option \"" + option + "\"");
1053 throw new IllegalArgumentException();
1054 }
1055 }
1056 handleUndeclaredRelations(lineNum, s, nameToVar, extras, rt);
1057 return solver.comeFromQuery(rt, extras, single);
1058 }
1059 List
1060 Map varMap = new LinkedHashMap();
1061 for (;;) {
1062 RuleTerm rt = parseRuleTerm(lineNum, s, nameToVar, st);
1063 if (rt == null) break;
1064 terms.add(rt);
1065 for (Iterator i = rt.variables.iterator(); i.hasNext(); ) {
1066 Variable v = (Variable) i.next();
1067 if (v.name.equals("_") || v.name.equals("*")) continue;
1068 String name;
1069 if (v instanceof Constant) {
1070 name = rt.relation.getAttribute(rt.variables.indexOf(v)).attributeName;
1071
1072 continue;
1073 } else {
1074 name = v.toString();
1075 }
1076 varMap.put(v, name);
1077 }
1078 String sep = nextToken(st);
1079 if (sep.equals("?")) break;
1080 if (!sep.equals(",")) {
1081 outputError(lineNum, st.getPosition(), s,
1082 "Expected \",\", got \"" + sep + "\"");
1083 throw new IllegalArgumentException();
1084 }
1085 }
1086 HashSet projections = new HashSet();
1087 while (st.hasMoreTokens()) {
1088 String option = nextToken(st);
1089 if (option.equals("project")) {
1090 boolean foundbrace = false;
1091 while (st.hasMoreTokens()) {
1092 option = nextToken(st);
1093 if (option.equals(";")) {
1094 foundbrace = true;
1095 break;
1096 }
1097 projections.add(option);
1098 }
1099 if (!foundbrace) {
1100 outputError(lineNum, st.getPosition(), s, "Expected query projection list terminator \";\"");
1101 throw new IllegalArgumentException();
1102 }
1103 } else {
1104 outputError(lineNum, st.getPosition(), s, "Unknown query option \"" + option + "\"");
1105 throw new IllegalArgumentException();
1106 }
1107 }
1108
1109 List vars = new ArrayList(varMap.keySet().size());
1110 List attributes = new ArrayList(vars.size());
1111 for (Iterator i = varMap.entrySet().iterator(); i.hasNext(); ) {
1112 Map.Entry e = (Map.Entry) i.next();
1113 Variable v = (Variable) e.getKey();
1114 String name = (String) e.getValue();
1115 if (!projections.contains(name)) {
1116 vars.add(v);
1117 attributes.add(new Attribute(name, v.getDomain(), ""));
1118 }
1119 }
1120 Relation r = solver.createRelation("query@"+lineNum, attributes);
1121 RuleTerm bottom = new RuleTerm(r, vars);
1122 handleUndeclaredRelations(lineNum, s, nameToVar, terms, bottom);
1123 InferenceRule ir = solver.createInferenceRule(terms, bottom);
1124 ir = parseRuleOptions(lineNum, s, ir, st);
1125 Variable v = ir.checkUnnecessaryVariables();
1126 if (v != null && !ALLOW_SINGLE_USE) {
1127 outputError(lineNum, st.getPosition(), s,
1128 "Variable "+v+" was only used once! Use '_' instead.");
1129 throw new IllegalArgumentException();
1130 }
1131 solver.relationsToPrintTuples.add(r);
1132 return Collections.singletonList(ir);
1133 }
1134
1135 }