00001
00002 package edu.tum.cs.logic.parser;
00003
00004 import java.util.*;
00005 import edu.tum.cs.logic.*;
00006 import java.io.*;
00007
00008 public @SuppressWarnings("all") class FormulaParser implements FormulaParserConstants {
00009 public static void main(String args[]) throws ParseException {
00010 String test;
00011 test = "foo(x,y) => !bar(x,zt) v baz(y)";
00012 test = "numberEats(o,2) <=> EXIST p, p2 (eats(o,p) ^ eats(o,p2) ^ !(o=p) ^ !(o=p2) ^ !(p=p2) ^ !(EXIST q (eats(o,q) ^ !(p=q) ^ !(p2=q))))";
00013 Formula f = parse(test);
00014 System.out.println("formula: " + f);
00015 }
00016
00017 public static Formula parse(String s) throws ParseException {
00018 FormulaParser parser = new FormulaParser(new StringReader(s));
00019 Formula f = parser.formula();
00020 Token t = parser.getNextToken();
00021 if(t.beginColumn != s.length())
00022 throw new ParseException("Unexpected token '" + t.toString() + "'");
00023 return f;
00024 }
00025
00026 final public String variable() throws ParseException {
00027 Token t;
00028 t = jj_consume_token(LCIDENT);
00029 {if (true) return t.image;}
00030 throw new Error("Missing return statement in function");
00031 }
00032
00033 final public String constant() throws ParseException {
00034 Token t;
00035 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00036 case UCIDENT:
00037 t = jj_consume_token(UCIDENT);
00038 break;
00039 case NUMBER:
00040 t = jj_consume_token(NUMBER);
00041 break;
00042 default:
00043 jj_la1[0] = jj_gen;
00044 jj_consume_token(-1);
00045 throw new ParseException();
00046 }
00047 {if (true) return t.image;}
00048 throw new Error("Missing return statement in function");
00049 }
00050
00051 final public Collection<String> paramlist() throws ParseException {
00052 Collection<String> ret;
00053 String arg;
00054 ret = new Vector<String>();
00055 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00056 case LCIDENT:
00057 arg = variable();
00058 break;
00059 case NUMBER:
00060 case UCIDENT:
00061 arg = constant();
00062 break;
00063 default:
00064 jj_la1[1] = jj_gen;
00065 jj_consume_token(-1);
00066 throw new ParseException();
00067 }
00068 ret.add(arg);
00069 label_1:
00070 while (true) {
00071 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00072 case LISTSEP:
00073 ;
00074 break;
00075 default:
00076 jj_la1[2] = jj_gen;
00077 break label_1;
00078 }
00079 jj_consume_token(LISTSEP);
00080 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00081 case LCIDENT:
00082 arg = variable();
00083 break;
00084 case NUMBER:
00085 case UCIDENT:
00086 arg = constant();
00087 break;
00088 default:
00089 jj_la1[3] = jj_gen;
00090 jj_consume_token(-1);
00091 throw new ParseException();
00092 }
00093 ret.add(arg);
00094 }
00095 {if (true) return ret;}
00096 throw new Error("Missing return statement in function");
00097 }
00098
00099 final public Collection<String> varlist() throws ParseException {
00100 Collection<String> ret;
00101 String arg;
00102 ret = new Vector<String>();
00103 arg = variable();
00104 ret.add(arg);
00105 label_2:
00106 while (true) {
00107 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00108 case LISTSEP:
00109 ;
00110 break;
00111 default:
00112 jj_la1[4] = jj_gen;
00113 break label_2;
00114 }
00115 jj_consume_token(LISTSEP);
00116 arg = variable();
00117 ret.add(arg);
00118 }
00119 {if (true) return ret;}
00120 throw new Error("Missing return statement in function");
00121 }
00122
00123 final public String predName() throws ParseException {
00124 Token t;
00125 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00126 case LCIDENT:
00127 t = jj_consume_token(LCIDENT);
00128 break;
00129 case UCIDENT:
00130 t = jj_consume_token(UCIDENT);
00131 break;
00132 default:
00133 jj_la1[5] = jj_gen;
00134 jj_consume_token(-1);
00135 throw new ParseException();
00136 }
00137 {if (true) return t.image;}
00138 throw new Error("Missing return statement in function");
00139 }
00140
00141 final public Atom atom() throws ParseException {
00142 Token t;
00143 String predName;
00144 Collection<String> params;
00145 predName = predName();
00146 jj_consume_token(OPENRB);
00147 params = paramlist();
00148 jj_consume_token(CLOSERB);
00149 {if (true) return new Atom(predName, params);}
00150 throw new Error("Missing return statement in function");
00151 }
00152
00153 final public Literal literal() throws ParseException {
00154 Atom atom;
00155 boolean isTrue;
00156 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00157 case UCIDENT:
00158 case LCIDENT:
00159 atom = atom();
00160 isTrue = true;
00161 break;
00162 case NOT:
00163 jj_consume_token(NOT);
00164 atom = atom();
00165 isTrue = false;
00166 break;
00167 default:
00168 jj_la1[6] = jj_gen;
00169 jj_consume_token(-1);
00170 throw new ParseException();
00171 }
00172 {if (true) return new Literal(isTrue, atom);}
00173 throw new Error("Missing return statement in function");
00174 }
00175
00176 final public Negation negation() throws ParseException {
00177 Formula f;
00178 jj_consume_token(NOT);
00179 jj_consume_token(OPENRB);
00180 f = formula();
00181 jj_consume_token(CLOSERB);
00182 {if (true) return new Negation(f);}
00183 throw new Error("Missing return statement in function");
00184 }
00185
00186 final public Exist exist() throws ParseException {
00187 Formula f;
00188 Collection<String> vars;
00189 jj_consume_token(EXIST);
00190 vars = varlist();
00191 jj_consume_token(OPENRB);
00192 f = formula();
00193 jj_consume_token(CLOSERB);
00194 {if (true) return new Exist(vars, f);}
00195 throw new Error("Missing return statement in function");
00196 }
00197
00198 final public ForAll forall() throws ParseException {
00199 Formula f;
00200 Collection<String> vars;
00201 jj_consume_token(FORALL);
00202 vars = varlist();
00203 jj_consume_token(OPENRB);
00204 f = formula();
00205 jj_consume_token(CLOSERB);
00206 {if (true) return new ForAll(vars, f);}
00207 throw new Error("Missing return statement in function");
00208 }
00209
00210 final public Equality equality() throws ParseException {
00211 String left, right;
00212 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00213 case LCIDENT:
00214 left = variable();
00215 break;
00216 case NUMBER:
00217 case UCIDENT:
00218 left = constant();
00219 break;
00220 default:
00221 jj_la1[7] = jj_gen;
00222 jj_consume_token(-1);
00223 throw new ParseException();
00224 }
00225 jj_consume_token(EQUALS);
00226 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00227 case LCIDENT:
00228 right = variable();
00229 break;
00230 case NUMBER:
00231 case UCIDENT:
00232 right = constant();
00233 break;
00234 default:
00235 jj_la1[8] = jj_gen;
00236 jj_consume_token(-1);
00237 throw new ParseException();
00238 }
00239 {if (true) return new Equality(left, right);}
00240 throw new Error("Missing return statement in function");
00241 }
00242
00243 final public Formula formulaElement() throws ParseException {
00244 Formula f;
00245 if (jj_2_1(2147483647)) {
00246 f = negation();
00247 } else if (jj_2_2(2147483647)) {
00248 f = equality();
00249 } else {
00250 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00251 case NOT:
00252 case UCIDENT:
00253 case LCIDENT:
00254 f = literal();
00255 break;
00256 case OPENRB:
00257 jj_consume_token(OPENRB);
00258 f = formula();
00259 jj_consume_token(CLOSERB);
00260 break;
00261 case EXIST:
00262 f = exist();
00263 break;
00264 case FORALL:
00265 f = forall();
00266 break;
00267 default:
00268 jj_la1[9] = jj_gen;
00269 jj_consume_token(-1);
00270 throw new ParseException();
00271 }
00272 }
00273 {if (true) return f;}
00274 throw new Error("Missing return statement in function");
00275 }
00276
00277 final public Formula disjunction() throws ParseException {
00278 Formula f;
00279 Vector<Formula> children;
00280 children = new Vector<Formula>();
00281 f = formulaElement();
00282 children.add(f);
00283 label_3:
00284 while (true) {
00285 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00286 case OR:
00287 ;
00288 break;
00289 default:
00290 jj_la1[10] = jj_gen;
00291 break label_3;
00292 }
00293 jj_consume_token(OR);
00294 f = formulaElement();
00295 children.add(f);
00296 }
00297 {if (true) return children.size() > 1 ? new Disjunction(children) : f;}
00298 throw new Error("Missing return statement in function");
00299 }
00300
00301 final public Formula conjunction() throws ParseException {
00302 Formula f;
00303 Vector<Formula> children;
00304 children = new Vector<Formula>();
00305 f = disjunction();
00306 children.add(f);
00307 label_4:
00308 while (true) {
00309 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00310 case AND:
00311 ;
00312 break;
00313 default:
00314 jj_la1[11] = jj_gen;
00315 break label_4;
00316 }
00317 jj_consume_token(AND);
00318 f = disjunction();
00319 children.add(f);
00320 }
00321 {if (true) return children.size() > 1 ? new Conjunction(children) : f;}
00322 throw new Error("Missing return statement in function");
00323 }
00324
00325 final public Formula implication() throws ParseException {
00326 Formula f1, f2;
00327 f2 = null;
00328 f1 = conjunction();
00329 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00330 case IMPLIES:
00331 jj_consume_token(IMPLIES);
00332 f2 = conjunction();
00333 break;
00334 default:
00335 jj_la1[12] = jj_gen;
00336 ;
00337 }
00338 {if (true) return f2 == null ? f1 : new Implication(f1, f2);}
00339 throw new Error("Missing return statement in function");
00340 }
00341
00342 final public Formula biimplication() throws ParseException {
00343 Formula f1, f2;
00344 f2 = null;
00345 f1 = implication();
00346 switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
00347 case IFF:
00348 jj_consume_token(IFF);
00349 f2 = implication();
00350 break;
00351 default:
00352 jj_la1[13] = jj_gen;
00353 ;
00354 }
00355 {if (true) return f2 == null ? f1 : new Biimplication(f1, f2);}
00356 throw new Error("Missing return statement in function");
00357 }
00358
00359 final public Formula formula() throws ParseException {
00360 Formula f;
00361 f = biimplication();
00362 {if (true) return f;}
00363 throw new Error("Missing return statement in function");
00364 }
00365
00366 final private boolean jj_2_1(int xla) {
00367 jj_la = xla; jj_lastpos = jj_scanpos = token;
00368 try { return !jj_3_1(); }
00369 catch(LookaheadSuccess ls) { return true; }
00370 finally { jj_save(0, xla); }
00371 }
00372
00373 final private boolean jj_2_2(int xla) {
00374 jj_la = xla; jj_lastpos = jj_scanpos = token;
00375 try { return !jj_3_2(); }
00376 catch(LookaheadSuccess ls) { return true; }
00377 finally { jj_save(1, xla); }
00378 }
00379
00380 final private boolean jj_3_2() {
00381 if (jj_3R_5()) return true;
00382 return false;
00383 }
00384
00385 final private boolean jj_3_1() {
00386 if (jj_scan_token(NOT)) return true;
00387 if (jj_scan_token(OPENRB)) return true;
00388 return false;
00389 }
00390
00391 final private boolean jj_3R_8() {
00392 if (jj_3R_10()) return true;
00393 return false;
00394 }
00395
00396 final private boolean jj_3R_11() {
00397 Token xsp;
00398 xsp = jj_scanpos;
00399 if (jj_scan_token(21)) {
00400 jj_scanpos = xsp;
00401 if (jj_scan_token(20)) return true;
00402 }
00403 return false;
00404 }
00405
00406 final private boolean jj_3R_6() {
00407 if (jj_3R_10()) return true;
00408 return false;
00409 }
00410
00411 final private boolean jj_3R_9() {
00412 if (jj_3R_11()) return true;
00413 return false;
00414 }
00415
00416 final private boolean jj_3R_10() {
00417 if (jj_scan_token(LCIDENT)) return true;
00418 return false;
00419 }
00420
00421 final private boolean jj_3R_5() {
00422 Token xsp;
00423 xsp = jj_scanpos;
00424 if (jj_3R_6()) {
00425 jj_scanpos = xsp;
00426 if (jj_3R_7()) return true;
00427 }
00428 if (jj_scan_token(EQUALS)) return true;
00429 xsp = jj_scanpos;
00430 if (jj_3R_8()) {
00431 jj_scanpos = xsp;
00432 if (jj_3R_9()) return true;
00433 }
00434 return false;
00435 }
00436
00437 final private boolean jj_3R_7() {
00438 if (jj_3R_11()) return true;
00439 return false;
00440 }
00441
00442 public FormulaParserTokenManager token_source;
00443 SimpleCharStream jj_input_stream;
00444 public Token token, jj_nt;
00445 private int jj_ntk;
00446 private Token jj_scanpos, jj_lastpos;
00447 private int jj_la;
00448 public boolean lookingAhead = false;
00449 private boolean jj_semLA;
00450 private int jj_gen;
00451 final private int[] jj_la1 = new int[14];
00452 static private int[] jj_la1_0;
00453 static {
00454 jj_la1_0();
00455 }
00456 private static void jj_la1_0() {
00457 jj_la1_0 = new int[] {0x300000,0x700000,0x8000,0x700000,0x8000,0x600000,0x600020,0x700000,0x700000,0x603820,0x40,0x80,0x100,0x400,};
00458 }
00459 final private JJCalls[] jj_2_rtns = new JJCalls[2];
00460 private boolean jj_rescan = false;
00461 private int jj_gc = 0;
00462
00463 public FormulaParser(java.io.InputStream stream) {
00464 this(stream, null);
00465 }
00466 public FormulaParser(java.io.InputStream stream, String encoding) {
00467 try { jj_input_stream = new SimpleCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
00468 token_source = new FormulaParserTokenManager(jj_input_stream);
00469 token = new Token();
00470 jj_ntk = -1;
00471 jj_gen = 0;
00472 for (int i = 0; i < 14; i++) jj_la1[i] = -1;
00473 for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
00474 }
00475
00476 public void ReInit(java.io.InputStream stream) {
00477 ReInit(stream, null);
00478 }
00479 public void ReInit(java.io.InputStream stream, String encoding) {
00480 try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
00481 token_source.ReInit(jj_input_stream);
00482 token = new Token();
00483 jj_ntk = -1;
00484 jj_gen = 0;
00485 for (int i = 0; i < 14; i++) jj_la1[i] = -1;
00486 for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
00487 }
00488
00489 public FormulaParser(java.io.Reader stream) {
00490 jj_input_stream = new SimpleCharStream(stream, 1, 1);
00491 token_source = new FormulaParserTokenManager(jj_input_stream);
00492 token = new Token();
00493 jj_ntk = -1;
00494 jj_gen = 0;
00495 for (int i = 0; i < 14; i++) jj_la1[i] = -1;
00496 for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
00497 }
00498
00499 public void ReInit(java.io.Reader stream) {
00500 jj_input_stream.ReInit(stream, 1, 1);
00501 token_source.ReInit(jj_input_stream);
00502 token = new Token();
00503 jj_ntk = -1;
00504 jj_gen = 0;
00505 for (int i = 0; i < 14; i++) jj_la1[i] = -1;
00506 for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
00507 }
00508
00509 public FormulaParser(FormulaParserTokenManager tm) {
00510 token_source = tm;
00511 token = new Token();
00512 jj_ntk = -1;
00513 jj_gen = 0;
00514 for (int i = 0; i < 14; i++) jj_la1[i] = -1;
00515 for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
00516 }
00517
00518 public void ReInit(FormulaParserTokenManager tm) {
00519 token_source = tm;
00520 token = new Token();
00521 jj_ntk = -1;
00522 jj_gen = 0;
00523 for (int i = 0; i < 14; i++) jj_la1[i] = -1;
00524 for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
00525 }
00526
00527 final private Token jj_consume_token(int kind) throws ParseException {
00528 Token oldToken;
00529 if ((oldToken = token).next != null) token = token.next;
00530 else token = token.next = token_source.getNextToken();
00531 jj_ntk = -1;
00532 if (token.kind == kind) {
00533 jj_gen++;
00534 if (++jj_gc > 100) {
00535 jj_gc = 0;
00536 for (int i = 0; i < jj_2_rtns.length; i++) {
00537 JJCalls c = jj_2_rtns[i];
00538 while (c != null) {
00539 if (c.gen < jj_gen) c.first = null;
00540 c = c.next;
00541 }
00542 }
00543 }
00544 return token;
00545 }
00546 token = oldToken;
00547 jj_kind = kind;
00548 throw generateParseException();
00549 }
00550
00551 static private final class LookaheadSuccess extends java.lang.Error { }
00552 final private LookaheadSuccess jj_ls = new LookaheadSuccess();
00553 final private boolean jj_scan_token(int kind) {
00554 if (jj_scanpos == jj_lastpos) {
00555 jj_la--;
00556 if (jj_scanpos.next == null) {
00557 jj_lastpos = jj_scanpos = jj_scanpos.next = token_source.getNextToken();
00558 } else {
00559 jj_lastpos = jj_scanpos = jj_scanpos.next;
00560 }
00561 } else {
00562 jj_scanpos = jj_scanpos.next;
00563 }
00564 if (jj_rescan) {
00565 int i = 0; Token tok = token;
00566 while (tok != null && tok != jj_scanpos) { i++; tok = tok.next; }
00567 if (tok != null) jj_add_error_token(kind, i);
00568 }
00569 if (jj_scanpos.kind != kind) return true;
00570 if (jj_la == 0 && jj_scanpos == jj_lastpos) throw jj_ls;
00571 return false;
00572 }
00573
00574 final public Token getNextToken() {
00575 if (token.next != null) token = token.next;
00576 else token = token.next = token_source.getNextToken();
00577 jj_ntk = -1;
00578 jj_gen++;
00579 return token;
00580 }
00581
00582 final public Token getToken(int index) {
00583 Token t = lookingAhead ? jj_scanpos : token;
00584 for (int i = 0; i < index; i++) {
00585 if (t.next != null) t = t.next;
00586 else t = t.next = token_source.getNextToken();
00587 }
00588 return t;
00589 }
00590
00591 final private int jj_ntk() {
00592 if ((jj_nt=token.next) == null)
00593 return (jj_ntk = (token.next=token_source.getNextToken()).kind);
00594 else
00595 return (jj_ntk = jj_nt.kind);
00596 }
00597
00598 private java.util.Vector<int[]> jj_expentries = new java.util.Vector<int[]>();
00599 private int[] jj_expentry;
00600 private int jj_kind = -1;
00601 private int[] jj_lasttokens = new int[100];
00602 private int jj_endpos;
00603
00604 private void jj_add_error_token(int kind, int pos) {
00605 if (pos >= 100) return;
00606 if (pos == jj_endpos + 1) {
00607 jj_lasttokens[jj_endpos++] = kind;
00608 } else if (jj_endpos != 0) {
00609 jj_expentry = new int[jj_endpos];
00610 for (int i = 0; i < jj_endpos; i++) {
00611 jj_expentry[i] = jj_lasttokens[i];
00612 }
00613 boolean exists = false;
00614 for (java.util.Enumeration e = jj_expentries.elements(); e.hasMoreElements();) {
00615 int[] oldentry = (int[])(e.nextElement());
00616 if (oldentry.length == jj_expentry.length) {
00617 exists = true;
00618 for (int i = 0; i < jj_expentry.length; i++) {
00619 if (oldentry[i] != jj_expentry[i]) {
00620 exists = false;
00621 break;
00622 }
00623 }
00624 if (exists) break;
00625 }
00626 }
00627 if (!exists) jj_expentries.addElement(jj_expentry);
00628 if (pos != 0) jj_lasttokens[(jj_endpos = pos) - 1] = kind;
00629 }
00630 }
00631
00632 public ParseException generateParseException() {
00633 jj_expentries.removeAllElements();
00634 boolean[] la1tokens = new boolean[23];
00635 if (jj_kind >= 0) {
00636 la1tokens[jj_kind] = true;
00637 jj_kind = -1;
00638 }
00639 for (int i = 0; i < 14; i++) {
00640 if (jj_la1[i] == jj_gen) {
00641 for (int j = 0; j < 32; j++) {
00642 if ((jj_la1_0[i] & (1<<j)) != 0) {
00643 la1tokens[j] = true;
00644 }
00645 }
00646 }
00647 }
00648 for (int i = 0; i < 23; i++) {
00649 if (la1tokens[i]) {
00650 jj_expentry = new int[1];
00651 jj_expentry[0] = i;
00652 jj_expentries.addElement(jj_expentry);
00653 }
00654 }
00655 jj_endpos = 0;
00656 jj_rescan_token();
00657 jj_add_error_token(0, 0);
00658 int[][] exptokseq = new int[jj_expentries.size()][];
00659 for (int i = 0; i < jj_expentries.size(); i++) {
00660 exptokseq[i] = jj_expentries.elementAt(i);
00661 }
00662 return new ParseException(token, exptokseq, tokenImage);
00663 }
00664
00665 final public void enable_tracing() {
00666 }
00667
00668 final public void disable_tracing() {
00669 }
00670
00671 final private void jj_rescan_token() {
00672 jj_rescan = true;
00673 for (int i = 0; i < 2; i++) {
00674 try {
00675 JJCalls p = jj_2_rtns[i];
00676 do {
00677 if (p.gen > jj_gen) {
00678 jj_la = p.arg; jj_lastpos = jj_scanpos = p.first;
00679 switch (i) {
00680 case 0: jj_3_1(); break;
00681 case 1: jj_3_2(); break;
00682 }
00683 }
00684 p = p.next;
00685 } while (p != null);
00686 } catch(LookaheadSuccess ls) { }
00687 }
00688 jj_rescan = false;
00689 }
00690
00691 final private void jj_save(int index, int xla) {
00692 JJCalls p = jj_2_rtns[index];
00693 while (p.gen > jj_gen) {
00694 if (p.next == null) { p = p.next = new JJCalls(); break; }
00695 p = p.next;
00696 }
00697 p.gen = jj_gen + xla - jj_la; p.first = token; p.arg = xla;
00698 }
00699
00700 static final class JJCalls {
00701 int gen;
00702 Token first;
00703 int arg;
00704 JJCalls next;
00705 }
00706
00707 }
