View Javadoc

1   // DatalogParser.java, created May 15, 2005 4:53:12 PM by jwhaley
2   // Copyright (C) 2004 John Whaley <jwhaley@alum.mit.edu>
3   // Licensed under the terms of the GNU LGPL; see COPYING for details.
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             // directive
144             parseDirective(in, lineNum, s);
145             return null;
146         }
147         MyStringTokenizer st = new MyStringTokenizer(s);
148         if (st.hasMoreTokens()) {
149             st.nextToken(); // name
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                     // field domain
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             // rule
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                 // query
188                 List/*<InferenceRule>*/ ir = parseQuery(lineNum, s);
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             // relation
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             //return null;
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             //handle error
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/*<String,Variable>*/ nameToVar = new HashMap();
597         undeclaredRelations.clear();
598         RuleTerm bottom = parseRuleTerm(lineNum, s, nameToVar, st);
599         String sep = nextToken(st);
600         List/*<RuleTerm>*/ terms = new LinkedList();
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                         // We didn't know the domain then, maybe we do now.
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                     // Handle other uses of this relation in this rule.
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                 // todo: maxiter=#
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/*<String,Variable>*/ nameToVar, MyStringTokenizer st) {
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             // "a = b".
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                 // "a => b".
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/*<Variable>*/ vars = new LinkedList();
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             // Implicit creation of relation.
965             List/*<Attribute>*/ attribs = new ArrayList(vars.size());
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/*<InferenceRule>*/ parseQuery(int lineNum, String s) {
1022         MyStringTokenizer st = new MyStringTokenizer(s, " \t(,/).=~!?<>", true);
1023         Map/*<String,Variable>*/ nameToVar = new HashMap();
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/*<RuleTerm>*/ extras = new LinkedList();
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/*<RuleTerm>*/ terms = new LinkedList();
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                     // todo: check this.
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 }