diff --git a/src/main/java/com/booleworks/logicng/io/parsers/PropositionalParserNew.java b/src/main/java/com/booleworks/logicng/io/parsers/PropositionalParserNew.java new file mode 100644 index 00000000..2bc28c7a --- /dev/null +++ b/src/main/java/com/booleworks/logicng/io/parsers/PropositionalParserNew.java @@ -0,0 +1,82 @@ +// SPDX-License-Identifier: Apache-2.0 and MIT +// Copyright 2015-2023 Christoph Zengler +// Copyright 2023-20xx BooleWorks GmbH + +package com.booleworks.logicng.io.parsers; + +import com.booleworks.logicng.formulas.Formula; +import com.booleworks.logicng.formulas.FormulaFactory; +import com.booleworks.logicng.io.parsers.javacc.BooleanFormulaParser; +import com.booleworks.logicng.io.parsers.javacc.ParseException; +import com.booleworks.logicng.io.parsers.javacc.TokenMgrError; + +import java.io.StringReader; + +/** + * A parser for propositional (including pseudo-Boolean) formulas. + *

+ * The syntax for pseudo Boolean formulas in LogicNG is: + *

+ * Brackets are {@code (} and {@code )}. For variable names, there are the + * following rules: + * + *

+ * A valid pseudo Boolean expression is of the form + * {@code c_1 * l_1 + ... + c_n * l_n R k} where the {@code c_i} are + * coefficients, {@code l_i} are literals, and {@code R} is one of + * {@code =, >, >=, <, <=}. + * @version 2.4.1 + * @since 1.0 + */ +public final class PropositionalParserNew { + + private final BooleanFormulaParser parser; + + /** + * Constructs a new parser for pseudo boolean formulas. + * @param f the formula factory + */ + public PropositionalParserNew(final FormulaFactory f) { + parser = new BooleanFormulaParser(new StringReader("")); + parser.setFactory(f); + } + + public Formula parse(final String input) throws ParserException { + if (input == null || input.isBlank()) { + return parser.getFactory().verum(); + } + try { + parser.ReInit(new StringReader(input)); + return parser.formula(); + } catch (final TokenMgrError e) { + throw new ParserException("lexer error", null); //TODO + } catch (final ParseException e) { + throw new ParserException("parser error", e); //TODO + } + } + + public FormulaFactory factory() { + return parser.getFactory(); + } +} diff --git a/src/main/java/com/booleworks/logicng/io/parsers/javacc/BooleanFormulaParser.java b/src/main/java/com/booleworks/logicng/io/parsers/javacc/BooleanFormulaParser.java new file mode 100644 index 00000000..f4e8c931 --- /dev/null +++ b/src/main/java/com/booleworks/logicng/io/parsers/javacc/BooleanFormulaParser.java @@ -0,0 +1,789 @@ +/* BooleanFormulaParser.java */ +/* Generated By:JavaCC: Do not edit this line. BooleanFormulaParser.java */ +package com.booleworks.logicng.io.parsers.javacc; + +import com.booleworks.logicng.formulas.*; +import com.booleworks.logicng.util.Pair; + +import java.util.ArrayList; +import java.util.LinkedHashSet; +import java.util.List; + +public class BooleanFormulaParser implements BooleanFormulaParserConstants { + + private FormulaFactory f; + + public void setFactory(final FormulaFactory f) { + this.f = f; + } + + public FormulaFactory getFactory() { + return this.f; + } + + final public Formula formula() throws ParseException {Formula formula; + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case 0:{ + jj_consume_token(0); +formula = f.verum(); + break; + } + case NUMBER: + case LITERAL: + case TRUE: + case FALSE: + case LBR: + case NOT:{ + formula = equiv(); + jj_consume_token(0); + break; + } + default: + jj_la1[0] = jj_gen; + jj_consume_token(-1); + throw new ParseException(); + } +{if ("" != null) return formula;} + throw new Error("Missing return statement in function"); +} + + final public Formula equiv() throws ParseException {Formula left; + Formula right = null; + left = impl(); + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case EQUIV:{ + jj_consume_token(EQUIV); + right = equiv(); + break; + } + default: + jj_la1[1] = jj_gen; + ; + } +{if ("" != null) return right == null ? left : f.equivalence(left, right);} + throw new Error("Missing return statement in function"); +} + + final public Formula impl() throws ParseException {Formula left; + Formula right = null; + left = disj(); + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case IMPL:{ + jj_consume_token(IMPL); + right = impl(); + break; + } + default: + jj_la1[2] = jj_gen; + ; + } +{if ("" != null) return right == null ? left : f.implication(left, right);} + throw new Error("Missing return statement in function"); +} + + final public Formula disj() throws ParseException {Formula a, b; + LinkedHashSet conjs = new LinkedHashSet<>(); + a = conj(); +conjs.add(a); + label_1: + while (true) { + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case OR:{ + ; + break; + } + default: + jj_la1[3] = jj_gen; + break label_1; + } + jj_consume_token(OR); + b = conj(); +conjs.add(b); + } +{if ("" != null) return f.or(conjs);} + throw new Error("Missing return statement in function"); +} + + final public Formula conj() throws ParseException {Formula a, b; + LinkedHashSet lits = new LinkedHashSet<>(); + a = lit(); +lits.add(a); + label_2: + while (true) { + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case AND:{ + ; + break; + } + default: + jj_la1[4] = jj_gen; + break label_2; + } + jj_consume_token(AND); + b = lit(); +lits.add(b); + } +{if ("" != null) return f.and(lits);} + throw new Error("Missing return statement in function"); +} + + final public Formula lit() throws ParseException {Formula formula, op; + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case NOT:{ + jj_consume_token(NOT); + op = lit(); +formula = f.not(op); + break; + } + case NUMBER: + case LITERAL: + case TRUE: + case FALSE: + case LBR:{ + formula = simp(); + break; + } + default: + jj_la1[5] = jj_gen; + jj_consume_token(-1); + throw new ParseException(); + } +{if ("" != null) return formula;} + throw new Error("Missing return statement in function"); +} + + final public Formula simp() throws ParseException {Formula formula; + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case NUMBER: + case LITERAL:{ + formula = comparison(); + break; + } + case TRUE: + case FALSE:{ + formula = constant(); + break; + } + case LBR:{ + jj_consume_token(LBR); + formula = equiv(); + jj_consume_token(RBR); + break; + } + default: + jj_la1[6] = jj_gen; + jj_consume_token(-1); + throw new ParseException(); + } +{if ("" != null) return formula;} + throw new Error("Missing return statement in function"); +} + + final public Formula comparison() throws ParseException {Formula formula; + Pair, List> e; + CType c; + Token t; + if (jj_2_1(2)) { + e = add(); + c = comperator(); + t = jj_consume_token(NUMBER); +formula = f.pbc(c, Integer.parseInt(t.image), e.first(), e.second()); + } else { + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case NUMBER:{ + t = jj_consume_token(NUMBER); +formula = (t.image.startsWith("~") ? f.literal(t.image.substring(1), false) : f.literal(t.image, true)); + break; + } + case LITERAL:{ + t = jj_consume_token(LITERAL); +formula = (t.image.startsWith("~") ? f.literal(t.image.substring(1), false) : f.literal(t.image, true)); + break; + } + default: + jj_la1[7] = jj_gen; + jj_consume_token(-1); + throw new ParseException(); + } + } +{if ("" != null) return formula;} + throw new Error("Missing return statement in function"); +} + + final public CType comperator() throws ParseException { + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case EQ:{ + jj_consume_token(EQ); +{if ("" != null) return CType.EQ;} + break; + } + case LE:{ + jj_consume_token(LE); +{if ("" != null) return CType.LE;} + break; + } + case LT:{ + jj_consume_token(LT); +{if ("" != null) return CType.LT;} + break; + } + case GE:{ + jj_consume_token(GE); +{if ("" != null) return CType.GE;} + break; + } + case GT:{ + jj_consume_token(GT); +{if ("" != null) return CType.GT;} + break; + } + default: + jj_la1[8] = jj_gen; + jj_consume_token(-1); + throw new ParseException(); + } + throw new Error("Missing return statement in function"); +} + + final public Pair, List> add() throws ParseException {Pair m1, m2; + List lits = new ArrayList<>(); + List coeffs = new ArrayList<>(); + Token a; + m1 = mul(); +lits.add(m1.first()); coeffs.add(m1.second()); + label_3: + while (true) { + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case ADD:{ + ; + break; + } + default: + jj_la1[9] = jj_gen; + break label_3; + } + a = jj_consume_token(ADD); + m2 = mul(); +lits.add(m2.first()); coeffs.add (a.image.equals("+") ? m2.second() : -m2.second()); + } +{if ("" != null) return new Pair<>(lits, coeffs);} + throw new Error("Missing return statement in function"); +} + + final public Pair mul() throws ParseException {Token n, l; + Literal lit; + int c = 1; + if (jj_2_2(3)) { + n = jj_consume_token(NUMBER); + jj_consume_token(MUL); + l = jj_consume_token(LITERAL); +lit = (l.image.startsWith("~") ? f.literal(l.image.substring(1), false) : f .literal(l.image, true)); c = Integer.parseInt(n.image); + } else if (jj_2_3(3)) { + n = jj_consume_token(NUMBER); + jj_consume_token(MUL); + l = jj_consume_token(NUMBER); +lit = f.literal(l.image, true); c = Integer.parseInt(n.image); + } else { + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case LITERAL:{ + l = jj_consume_token(LITERAL); +lit = (l.image.startsWith("~") ? f.literal(l.image.substring(1), false) : f.literal (l.image, true) ); + break; + } + case NUMBER:{ + n = jj_consume_token(NUMBER); +lit = f.literal(n.image, true); + break; + } + default: + jj_la1[10] = jj_gen; + jj_consume_token(-1); + throw new ParseException(); + } + } +{if ("" != null) return new Pair<>(lit, c);} + throw new Error("Missing return statement in function"); +} + + final public Formula constant() throws ParseException { + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { + case TRUE:{ + jj_consume_token(TRUE); +{if ("" != null) return f.verum();} + break; + } + case FALSE:{ + jj_consume_token(FALSE); +{if ("" != null) return f.falsum();} + break; + } + default: + jj_la1[11] = jj_gen; + jj_consume_token(-1); + throw new ParseException(); + } + throw new Error("Missing return statement in function"); +} + + private boolean jj_2_1(int xla) + { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return (!jj_3_1()); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(0, xla); } + } + + private boolean jj_2_2(int xla) + { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return (!jj_3_2()); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(1, xla); } + } + + private boolean jj_2_3(int xla) + { + jj_la = xla; jj_lastpos = jj_scanpos = token; + try { return (!jj_3_3()); } + catch(LookaheadSuccess ls) { return true; } + finally { jj_save(2, xla); } + } + + private boolean jj_3_3() + { + if (jj_scan_token(NUMBER)) return true; + if (jj_scan_token(MUL)) return true; + if (jj_scan_token(NUMBER)) return true; + return false; + } + + private boolean jj_3_2() + { + if (jj_scan_token(NUMBER)) return true; + if (jj_scan_token(MUL)) return true; + if (jj_scan_token(LITERAL)) return true; + return false; + } + + private boolean jj_3R_comperator_130_5_5() + { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_comperator_130_5_8()) { + jj_scanpos = xsp; + if (jj_3R_comperator_131_7_9()) { + jj_scanpos = xsp; + if (jj_3R_comperator_132_7_10()) { + jj_scanpos = xsp; + if (jj_3R_comperator_133_7_11()) { + jj_scanpos = xsp; + if (jj_3R_comperator_134_7_12()) return true; + } + } + } + } + return false; + } + + private boolean jj_3R_comperator_130_5_8() + { + if (jj_scan_token(EQ)) return true; + return false; + } + + private boolean jj_3R_mul_154_3_6() + { + Token xsp; + xsp = jj_scanpos; + if (jj_3_2()) { + jj_scanpos = xsp; + if (jj_3_3()) { + jj_scanpos = xsp; + if (jj_3R_mul_156_5_13()) { + jj_scanpos = xsp; + if (jj_3R_mul_157_5_14()) return true; + } + } + } + return false; + } + + private boolean jj_3_1() + { + if (jj_3R_add_144_3_4()) return true; + if (jj_3R_comperator_130_5_5()) return true; + return false; + } + + private boolean jj_3R_add_144_3_4() + { + if (jj_3R_mul_154_3_6()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_add_144_66_7()) { jj_scanpos = xsp; break; } + } + return false; + } + + private boolean jj_3R_comperator_134_7_12() + { + if (jj_scan_token(GT)) return true; + return false; + } + + private boolean jj_3R_add_144_66_7() + { + if (jj_scan_token(ADD)) return true; + return false; + } + + private boolean jj_3R_comperator_133_7_11() + { + if (jj_scan_token(GE)) return true; + return false; + } + + private boolean jj_3R_mul_157_5_14() + { + if (jj_scan_token(NUMBER)) return true; + return false; + } + + private boolean jj_3R_comperator_132_7_10() + { + if (jj_scan_token(LT)) return true; + return false; + } + + private boolean jj_3R_mul_156_5_13() + { + if (jj_scan_token(LITERAL)) return true; + return false; + } + + private boolean jj_3R_comperator_131_7_9() + { + if (jj_scan_token(LE)) return true; + return false; + } + + /** Generated Token Manager. */ + public BooleanFormulaParserTokenManager token_source; + SimpleCharStream jj_input_stream; + /** Current token. */ + public Token token; + /** Next token. */ + public Token jj_nt; + private int jj_ntk; + private Token jj_scanpos, jj_lastpos; + private int jj_la; + private int jj_gen; + final private int[] jj_la1 = new int[12]; + static private int[] jj_la1_0; + static { + jj_la1_init_0(); + } + private static void jj_la1_init_0() { + jj_la1_0 = new int[] {0xbe1,0x8000,0x4000,0x2000,0x1000,0xbe0,0x3e0,0x60,0x7c0000,0x20000,0x60,0x180,}; + } + final private JJCalls[] jj_2_rtns = new JJCalls[3]; + private boolean jj_rescan = false; + private int jj_gc = 0; + + /** Constructor with InputStream. */ + public BooleanFormulaParser(java.io.InputStream stream) { + this(stream, null); + } + /** Constructor with InputStream and supplied encoding */ + public BooleanFormulaParser(java.io.InputStream stream, String encoding) { + try { jj_input_stream = new SimpleCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); } + token_source = new BooleanFormulaParserTokenManager(jj_input_stream); + token = new Token(); + jj_ntk = -1; + jj_gen = 0; + for (int i = 0; i < 12; i++) jj_la1[i] = -1; + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); + } + + /** Reinitialise. */ + public void ReInit(java.io.InputStream stream) { + ReInit(stream, null); + } + /** Reinitialise. */ + public void ReInit(java.io.InputStream stream, String encoding) { + try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); } + token_source.ReInit(jj_input_stream); + token = new Token(); + jj_ntk = -1; + jj_gen = 0; + for (int i = 0; i < 12; i++) jj_la1[i] = -1; + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); + } + + /** Constructor. */ + public BooleanFormulaParser(java.io.Reader stream) { + jj_input_stream = new SimpleCharStream(stream, 1, 1); + token_source = new BooleanFormulaParserTokenManager(jj_input_stream); + token = new Token(); + jj_ntk = -1; + jj_gen = 0; + for (int i = 0; i < 12; i++) jj_la1[i] = -1; + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); + } + + /** Reinitialise. */ + public void ReInit(java.io.Reader stream) { + if (jj_input_stream == null) { + jj_input_stream = new SimpleCharStream(stream, 1, 1); + } else { + jj_input_stream.ReInit(stream, 1, 1); + } + if (token_source == null) { + token_source = new BooleanFormulaParserTokenManager(jj_input_stream); + } + + token_source.ReInit(jj_input_stream); + token = new Token(); + jj_ntk = -1; + jj_gen = 0; + for (int i = 0; i < 12; i++) jj_la1[i] = -1; + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); + } + + /** Constructor with generated Token Manager. */ + public BooleanFormulaParser(BooleanFormulaParserTokenManager tm) { + token_source = tm; + token = new Token(); + jj_ntk = -1; + jj_gen = 0; + for (int i = 0; i < 12; i++) jj_la1[i] = -1; + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); + } + + /** Reinitialise. */ + public void ReInit(BooleanFormulaParserTokenManager tm) { + token_source = tm; + token = new Token(); + jj_ntk = -1; + jj_gen = 0; + for (int i = 0; i < 12; i++) jj_la1[i] = -1; + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); + } + + private Token jj_consume_token(int kind) throws ParseException { + Token oldToken; + if ((oldToken = token).next != null) token = token.next; + else token = token.next = token_source.getNextToken(); + jj_ntk = -1; + if (token.kind == kind) { + jj_gen++; + if (++jj_gc > 100) { + jj_gc = 0; + for (int i = 0; i < jj_2_rtns.length; i++) { + JJCalls c = jj_2_rtns[i]; + while (c != null) { + if (c.gen < jj_gen) c.first = null; + c = c.next; + } + } + } + return token; + } + token = oldToken; + jj_kind = kind; + throw generateParseException(); + } + + @SuppressWarnings("serial") + static private final class LookaheadSuccess extends java.lang.Error { + @Override + public Throwable fillInStackTrace() { + return this; + } + } + static private final LookaheadSuccess jj_ls = new LookaheadSuccess(); + private boolean jj_scan_token(int kind) { + if (jj_scanpos == jj_lastpos) { + jj_la--; + if (jj_scanpos.next == null) { + jj_lastpos = jj_scanpos = jj_scanpos.next = token_source.getNextToken(); + } else { + jj_lastpos = jj_scanpos = jj_scanpos.next; + } + } else { + jj_scanpos = jj_scanpos.next; + } + if (jj_rescan) { + int i = 0; Token tok = token; + while (tok != null && tok != jj_scanpos) { i++; tok = tok.next; } + if (tok != null) jj_add_error_token(kind, i); + } + if (jj_scanpos.kind != kind) return true; + if (jj_la == 0 && jj_scanpos == jj_lastpos) throw jj_ls; + return false; + } + + +/** Get the next Token. */ + final public Token getNextToken() { + if (token.next != null) token = token.next; + else token = token.next = token_source.getNextToken(); + jj_ntk = -1; + jj_gen++; + return token; + } + +/** Get the specific Token. */ + final public Token getToken(int index) { + Token t = token; + for (int i = 0; i < index; i++) { + if (t.next != null) t = t.next; + else t = t.next = token_source.getNextToken(); + } + return t; + } + + private int jj_ntk_f() { + if ((jj_nt=token.next) == null) + return (jj_ntk = (token.next=token_source.getNextToken()).kind); + else + return (jj_ntk = jj_nt.kind); + } + + private java.util.List jj_expentries = new java.util.ArrayList(); + private int[] jj_expentry; + private int jj_kind = -1; + private int[] jj_lasttokens = new int[100]; + private int jj_endpos; + + private void jj_add_error_token(int kind, int pos) { + if (pos >= 100) { + return; + } + + if (pos == jj_endpos + 1) { + jj_lasttokens[jj_endpos++] = kind; + } else if (jj_endpos != 0) { + jj_expentry = new int[jj_endpos]; + + for (int i = 0; i < jj_endpos; i++) { + jj_expentry[i] = jj_lasttokens[i]; + } + + for (int[] oldentry : jj_expentries) { + if (oldentry.length == jj_expentry.length) { + boolean isMatched = true; + + for (int i = 0; i < jj_expentry.length; i++) { + if (oldentry[i] != jj_expentry[i]) { + isMatched = false; + break; + } + + } + if (isMatched) { + jj_expentries.add(jj_expentry); + break; + } + } + } + + if (pos != 0) { + jj_lasttokens[(jj_endpos = pos) - 1] = kind; + } + } + } + + /** Generate ParseException. */ + public ParseException generateParseException() { + jj_expentries.clear(); + boolean[] la1tokens = new boolean[23]; + if (jj_kind >= 0) { + la1tokens[jj_kind] = true; + jj_kind = -1; + } + for (int i = 0; i < 12; i++) { + if (jj_la1[i] == jj_gen) { + for (int j = 0; j < 32; j++) { + if ((jj_la1_0[i] & (1< jj_gen) { + jj_la = p.arg; jj_lastpos = jj_scanpos = p.first; + switch (i) { + case 0: jj_3_1(); break; + case 1: jj_3_2(); break; + case 2: jj_3_3(); break; + } + } + p = p.next; + } while (p != null); + + } catch(LookaheadSuccess ls) { } + } + jj_rescan = false; + } + + private void jj_save(int index, int xla) { + JJCalls p = jj_2_rtns[index]; + while (p.gen > jj_gen) { + if (p.next == null) { p = p.next = new JJCalls(); break; } + p = p.next; + } + + p.gen = jj_gen + xla - jj_la; + p.first = token; + p.arg = xla; + } + + static final class JJCalls { + int gen; + Token first; + int arg; + JJCalls next; + } + +} diff --git a/src/main/java/com/booleworks/logicng/io/parsers/javacc/BooleanFormulaParserConstants.java b/src/main/java/com/booleworks/logicng/io/parsers/javacc/BooleanFormulaParserConstants.java new file mode 100644 index 00000000..7e8545a3 --- /dev/null +++ b/src/main/java/com/booleworks/logicng/io/parsers/javacc/BooleanFormulaParserConstants.java @@ -0,0 +1,80 @@ +/* Generated By:JavaCC: Do not edit this line. BooleanFormulaParserConstants.java */ +package com.booleworks.logicng.io.parsers.javacc; + + +/** + * Token literal values and constants. + * Generated by org.javacc.parser.OtherFilesGen#start() + */ +public interface BooleanFormulaParserConstants { + + /** End of File. */ + int EOF = 0; + /** RegularExpression Id. */ + int NUMBER = 5; + /** RegularExpression Id. */ + int LITERAL = 6; + /** RegularExpression Id. */ + int TRUE = 7; + /** RegularExpression Id. */ + int FALSE = 8; + /** RegularExpression Id. */ + int LBR = 9; + /** RegularExpression Id. */ + int RBR = 10; + /** RegularExpression Id. */ + int NOT = 11; + /** RegularExpression Id. */ + int AND = 12; + /** RegularExpression Id. */ + int OR = 13; + /** RegularExpression Id. */ + int IMPL = 14; + /** RegularExpression Id. */ + int EQUIV = 15; + /** RegularExpression Id. */ + int MUL = 16; + /** RegularExpression Id. */ + int ADD = 17; + /** RegularExpression Id. */ + int EQ = 18; + /** RegularExpression Id. */ + int LE = 19; + /** RegularExpression Id. */ + int LT = 20; + /** RegularExpression Id. */ + int GE = 21; + /** RegularExpression Id. */ + int GT = 22; + + /** Lexical state. */ + int DEFAULT = 0; + + /** Literal token values. */ + String[] tokenImage = { + "", + "\" \"", + "\"\\t\"", + "\"\\n\"", + "\"\\r\"", + "", + "", + "\"$true\"", + "\"$false\"", + "\"(\"", + "\")\"", + "\"~\"", + "\"&\"", + "\"|\"", + "\"=>\"", + "\"<=>\"", + "\"*\"", + "", + "\"=\"", + "\"<=\"", + "\"<\"", + "\">=\"", + "\">\"", + }; + +} diff --git a/src/main/java/com/booleworks/logicng/io/parsers/javacc/BooleanFormulaParserTokenManager.java b/src/main/java/com/booleworks/logicng/io/parsers/javacc/BooleanFormulaParserTokenManager.java new file mode 100644 index 00000000..5b870db5 --- /dev/null +++ b/src/main/java/com/booleworks/logicng/io/parsers/javacc/BooleanFormulaParserTokenManager.java @@ -0,0 +1,540 @@ +/* BooleanFormulaParserTokenManager.java */ +/* Generated By:JavaCC: Do not edit this line. BooleanFormulaParserTokenManager.java */ +package com.booleworks.logicng.io.parsers.javacc; +import com.booleworks.logicng.formulas.*; +import com.booleworks.logicng.util.Pair; +import java.util.ArrayList; +import java.util.LinkedHashSet; +import java.util.List; + +/** Token Manager. */ +@SuppressWarnings ("unused") +public class BooleanFormulaParserTokenManager implements BooleanFormulaParserConstants { + + /** Debug output. */ + public java.io.PrintStream debugStream = System.out; + /** Set debug output. */ + public void setDebugStream(java.io.PrintStream ds) { debugStream = ds; } +private final int jjStopStringLiteralDfa_0(int pos, long active0){ + switch (pos) + { + case 0: + if ((active0 & 0x800L) != 0L) + return 3; + return -1; + default : + return -1; + } +} +private final int jjStartNfa_0(int pos, long active0){ + return jjMoveNfa_0(jjStopStringLiteralDfa_0(pos, active0), pos + 1); +} +private int jjStopAtPos(int pos, int kind) +{ + jjmatchedKind = kind; + jjmatchedPos = pos; + return pos + 1; +} +private int jjMoveStringLiteralDfa0_0(){ + switch(curChar) + { + case 36: + return jjMoveStringLiteralDfa1_0(0x180L); + case 38: + return jjStopAtPos(0, 12); + case 40: + return jjStopAtPos(0, 9); + case 41: + return jjStopAtPos(0, 10); + case 42: + return jjStopAtPos(0, 16); + case 60: + jjmatchedKind = 20; + return jjMoveStringLiteralDfa1_0(0x88000L); + case 61: + jjmatchedKind = 18; + return jjMoveStringLiteralDfa1_0(0x4000L); + case 62: + jjmatchedKind = 22; + return jjMoveStringLiteralDfa1_0(0x200000L); + case 124: + return jjStopAtPos(0, 13); + case 126: + return jjStartNfaWithStates_0(0, 11, 3); + default : + return jjMoveNfa_0(0, 0); + } +} +private int jjMoveStringLiteralDfa1_0(long active0){ + try { curChar = input_stream.readChar(); } + catch(java.io.IOException e) { + jjStopStringLiteralDfa_0(0, active0); + return 1; + } + switch(curChar) + { + case 61: + if ((active0 & 0x80000L) != 0L) + { + jjmatchedKind = 19; + jjmatchedPos = 1; + } + else if ((active0 & 0x200000L) != 0L) + return jjStopAtPos(1, 21); + return jjMoveStringLiteralDfa2_0(active0, 0x8000L); + case 62: + if ((active0 & 0x4000L) != 0L) + return jjStopAtPos(1, 14); + break; + case 102: + return jjMoveStringLiteralDfa2_0(active0, 0x100L); + case 116: + return jjMoveStringLiteralDfa2_0(active0, 0x80L); + default : + break; + } + return jjStartNfa_0(0, active0); +} +private int jjMoveStringLiteralDfa2_0(long old0, long active0){ + if (((active0 &= old0)) == 0L) + return jjStartNfa_0(0, old0); + try { curChar = input_stream.readChar(); } + catch(java.io.IOException e) { + jjStopStringLiteralDfa_0(1, active0); + return 2; + } + switch(curChar) + { + case 62: + if ((active0 & 0x8000L) != 0L) + return jjStopAtPos(2, 15); + break; + case 97: + return jjMoveStringLiteralDfa3_0(active0, 0x100L); + case 114: + return jjMoveStringLiteralDfa3_0(active0, 0x80L); + default : + break; + } + return jjStartNfa_0(1, active0); +} +private int jjMoveStringLiteralDfa3_0(long old0, long active0){ + if (((active0 &= old0)) == 0L) + return jjStartNfa_0(1, old0); + try { curChar = input_stream.readChar(); } + catch(java.io.IOException e) { + jjStopStringLiteralDfa_0(2, active0); + return 3; + } + switch(curChar) + { + case 108: + return jjMoveStringLiteralDfa4_0(active0, 0x100L); + case 117: + return jjMoveStringLiteralDfa4_0(active0, 0x80L); + default : + break; + } + return jjStartNfa_0(2, active0); +} +private int jjMoveStringLiteralDfa4_0(long old0, long active0){ + if (((active0 &= old0)) == 0L) + return jjStartNfa_0(2, old0); + try { curChar = input_stream.readChar(); } + catch(java.io.IOException e) { + jjStopStringLiteralDfa_0(3, active0); + return 4; + } + switch(curChar) + { + case 101: + if ((active0 & 0x80L) != 0L) + return jjStopAtPos(4, 7); + break; + case 115: + return jjMoveStringLiteralDfa5_0(active0, 0x100L); + default : + break; + } + return jjStartNfa_0(3, active0); +} +private int jjMoveStringLiteralDfa5_0(long old0, long active0){ + if (((active0 &= old0)) == 0L) + return jjStartNfa_0(3, old0); + try { curChar = input_stream.readChar(); } + catch(java.io.IOException e) { + jjStopStringLiteralDfa_0(4, active0); + return 5; + } + switch(curChar) + { + case 101: + if ((active0 & 0x100L) != 0L) + return jjStopAtPos(5, 8); + break; + default : + break; + } + return jjStartNfa_0(4, active0); +} +private int jjStartNfaWithStates_0(int pos, int kind, int state) +{ + jjmatchedKind = kind; + jjmatchedPos = pos; + try { curChar = input_stream.readChar(); } + catch(java.io.IOException e) { return pos + 1; } + return jjMoveNfa_0(state, pos + 1); +} +private int jjMoveNfa_0(int startState, int curPos) +{ + int startsAt = 0; + jjnewStateCnt = 5; + int i = 1; + jjstateSet[0] = startState; + int kind = 0x7fffffff; + for (;;) + { + if (++jjround == 0x7fffffff) + ReInitRounds(); + if (curChar < 64) + { + long l = 1L << curChar; + do + { + switch(jjstateSet[--i]) + { + case 0: + if ((0x3ff000800000000L & l) != 0L) + { + if (kind > 6) + kind = 6; + { jjCheckNAdd(3); } + } + else if ((0x280000000000L & l) != 0L) + { + if (kind > 17) + kind = 17; + } + if ((0x3ff000000000000L & l) != 0L) + { + if (kind > 5) + kind = 5; + { jjCheckNAdd(1); } + } + else if (curChar == 45) + { jjCheckNAdd(1); } + break; + case 1: + if ((0x3ff000000000000L & l) == 0L) + break; + if (kind > 5) + kind = 5; + { jjCheckNAdd(1); } + break; + case 3: + if ((0x3ff000800000000L & l) == 0L) + break; + if (kind > 6) + kind = 6; + { jjCheckNAdd(3); } + break; + case 4: + if ((0x280000000000L & l) != 0L && kind > 17) + kind = 17; + break; + default : break; + } + } while(i != startsAt); + } + else if (curChar < 128) + { + long l = 1L << (curChar & 077); + do + { + switch(jjstateSet[--i]) + { + case 0: + if ((0x7fffffe87ffffffL & l) != 0L) + { + if (kind > 6) + kind = 6; + { jjCheckNAdd(3); } + } + else if (curChar == 126) + { jjCheckNAdd(3); } + break; + case 2: + if (curChar == 126) + { jjCheckNAdd(3); } + break; + case 3: + if ((0x7fffffe87ffffffL & l) == 0L) + break; + kind = 6; + { jjCheckNAdd(3); } + break; + default : break; + } + } while(i != startsAt); + } + else + { + int i2 = (curChar & 0xff) >> 6; + long l2 = 1L << (curChar & 077); + do + { + switch(jjstateSet[--i]) + { + default : break; + } + } while(i != startsAt); + } + if (kind != 0x7fffffff) + { + jjmatchedKind = kind; + jjmatchedPos = curPos; + kind = 0x7fffffff; + } + ++curPos; + if ((i = jjnewStateCnt) == (startsAt = 5 - (jjnewStateCnt = startsAt))) + return curPos; + try { curChar = input_stream.readChar(); } + catch(java.io.IOException e) { return curPos; } + } +} + +/** Token literal values. */ +public static final String[] jjstrLiteralImages = { +"", null, null, null, null, null, null, "\44\164\162\165\145", +"\44\146\141\154\163\145", "\50", "\51", "\176", "\46", "\174", "\75\76", "\74\75\76", "\52", null, +"\75", "\74\75", "\74", "\76\75", "\76", }; +protected Token jjFillToken() +{ + final Token t; + final String curTokenImage; + final int beginLine; + final int endLine; + final int beginColumn; + final int endColumn; + String im = jjstrLiteralImages[jjmatchedKind]; + curTokenImage = (im == null) ? input_stream.GetImage() : im; + beginLine = input_stream.getBeginLine(); + beginColumn = input_stream.getBeginColumn(); + endLine = input_stream.getEndLine(); + endColumn = input_stream.getEndColumn(); + t = Token.newToken(jjmatchedKind, curTokenImage); + + t.beginLine = beginLine; + t.endLine = endLine; + t.beginColumn = beginColumn; + t.endColumn = endColumn; + + return t; +} +static final int[] jjnextStates = {0 +}; + +int curLexState = 0; +int defaultLexState = 0; +int jjnewStateCnt; +int jjround; +int jjmatchedPos; +int jjmatchedKind; + +/** Get the next Token. */ +public Token getNextToken() +{ + Token matchedToken; + int curPos = 0; + + EOFLoop : + for (;;) + { + try + { + curChar = input_stream.BeginToken(); + } + catch(Exception e) + { + jjmatchedKind = 0; + jjmatchedPos = -1; + matchedToken = jjFillToken(); + return matchedToken; + } + + try { input_stream.backup(0); + while (curChar <= 32 && (0x100002600L & (1L << curChar)) != 0L) + curChar = input_stream.BeginToken(); + } + catch (java.io.IOException e1) { continue EOFLoop; } + jjmatchedKind = 0x7fffffff; + jjmatchedPos = 0; + curPos = jjMoveStringLiteralDfa0_0(); + if (jjmatchedKind != 0x7fffffff) + { + if (jjmatchedPos + 1 < curPos) + input_stream.backup(curPos - jjmatchedPos - 1); + if ((jjtoToken[jjmatchedKind >> 6] & (1L << (jjmatchedKind & 077))) != 0L) + { + matchedToken = jjFillToken(); + return matchedToken; + } + else + { + continue EOFLoop; + } + } + int error_line = input_stream.getEndLine(); + int error_column = input_stream.getEndColumn(); + String error_after = null; + boolean EOFSeen = false; + try { input_stream.readChar(); input_stream.backup(1); } + catch (java.io.IOException e1) { + EOFSeen = true; + error_after = curPos <= 1 ? "" : input_stream.GetImage(); + if (curChar == '\n' || curChar == '\r') { + error_line++; + error_column = 0; + } + else + error_column++; + } + if (!EOFSeen) { + input_stream.backup(1); + error_after = curPos <= 1 ? "" : input_stream.GetImage(); + } + throw new TokenMgrError(EOFSeen, curLexState, error_line, error_column, error_after, curChar, TokenMgrError.LEXICAL_ERROR); + } +} + +void SkipLexicalActions(Token matchedToken) +{ + switch(jjmatchedKind) + { + default : + break; + } +} +void MoreLexicalActions() +{ + jjimageLen += (lengthOfMatch = jjmatchedPos + 1); + switch(jjmatchedKind) + { + default : + break; + } +} +void TokenLexicalActions(Token matchedToken) +{ + switch(jjmatchedKind) + { + default : + break; + } +} +private void jjCheckNAdd(int state) +{ + if (jjrounds[state] != jjround) + { + jjstateSet[jjnewStateCnt++] = state; + jjrounds[state] = jjround; + } +} +private void jjAddStates(int start, int end) +{ + do { + jjstateSet[jjnewStateCnt++] = jjnextStates[start]; + } while (start++ != end); +} +private void jjCheckNAddTwoStates(int state1, int state2) +{ + jjCheckNAdd(state1); + jjCheckNAdd(state2); +} + + /** Constructor. */ + public BooleanFormulaParserTokenManager(SimpleCharStream stream){ + + if (SimpleCharStream.staticFlag) + throw new Error("ERROR: Cannot use a static CharStream class with a non-static lexical analyzer."); + + input_stream = stream; + } + + /** Constructor. */ + public BooleanFormulaParserTokenManager (SimpleCharStream stream, int lexState){ + ReInit(stream); + SwitchTo(lexState); + } + + /** Reinitialise parser. */ + + public void ReInit(SimpleCharStream stream) + { + + + jjmatchedPos = + jjnewStateCnt = + 0; + curLexState = defaultLexState; + input_stream = stream; + ReInitRounds(); + } + + private void ReInitRounds() + { + int i; + jjround = 0x80000001; + for (i = 5; i-- > 0;) + jjrounds[i] = 0x80000000; + } + + /** Reinitialise parser. */ + public void ReInit(SimpleCharStream stream, int lexState) + + { + ReInit(stream); + SwitchTo(lexState); + } + + /** Switch to specified lex state. */ + public void SwitchTo(int lexState) + { + if (lexState >= 1 || lexState < 0) + throw new TokenMgrError("Error: Ignoring invalid lexical state : " + lexState + ". State unchanged.", TokenMgrError.INVALID_LEXICAL_STATE); + else + curLexState = lexState; + } + + +/** Lexer state names. */ +public static final String[] lexStateNames = { + "DEFAULT", +}; + +/** Lex State array. */ +public static final int[] jjnewLexState = { + -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, -1, +}; +static final long[] jjtoToken = { + 0x7fffe1L, +}; +static final long[] jjtoSkip = { + 0x1eL, +}; +static final long[] jjtoSpecial = { + 0x0L, +}; +static final long[] jjtoMore = { + 0x0L, +}; + protected SimpleCharStream input_stream; + + private final int[] jjrounds = new int[5]; + private final int[] jjstateSet = new int[2 * 5]; + private final StringBuilder jjimage = new StringBuilder(); + private StringBuilder image = jjimage; + private int jjimageLen; + private int lengthOfMatch; + protected int curChar; +} diff --git a/src/main/java/com/booleworks/logicng/io/parsers/javacc/BooleanParser.jj b/src/main/java/com/booleworks/logicng/io/parsers/javacc/BooleanParser.jj new file mode 100644 index 00000000..3213a9c4 --- /dev/null +++ b/src/main/java/com/booleworks/logicng/io/parsers/javacc/BooleanParser.jj @@ -0,0 +1,167 @@ +//noinspection UnreachableCode +options { + STATIC = false; +} + +PARSER_BEGIN(BooleanFormulaParser) +package com.booleworks.logicng.io.parsers.javacc; + +import com.booleworks.logicng.formulas.*; +import com.booleworks.logicng.util.Pair; + +import java.util.ArrayList; +import java.util.LinkedHashSet; +import java.util.List; + +public class BooleanFormulaParser { + + private FormulaFactory f; + + public void setFactory(final FormulaFactory f) { + this.f = f; + } + + public FormulaFactory getFactory() { + return this.f; + } +} + +PARSER_END(BooleanFormulaParser) + +SKIP : { " " | "\t" | "\n" | "\r" } + +TOKEN : +{ + + | < LITERAL : (["~"])? (["A"-"Z", "a"-"z", "0"-"9", "_", "@", "#"])+ > + | + | + | + | + | + | + | + | "> + | "> + | + | + | + | ="> + | "> +} + +Formula formula() : { Formula formula; } +{ + ( { formula = f.verum(); } + | formula = equiv() + ) + { return formula;} +} + +Formula equiv() : { + Formula left; + Formula right = null; +} +{ + left = impl() ( right = equiv() )? { return right == null ? left : f.equivalence(left, right); } +} + +Formula impl() : { + Formula left; + Formula right = null; +} +{ + left = disj() ( right = impl())? { return right == null ? left : f.implication(left, right); } +} + +Formula disj() : { + Formula a, b; + LinkedHashSet conjs = new LinkedHashSet<>(); +} +{ + a = conj() { conjs.add(a); } ( b = conj() { conjs.add(b); })* { return f.or(conjs); } +} + +Formula conj() : { + Formula a, b; + LinkedHashSet lits = new LinkedHashSet<>(); +} +{ + a = lit() { lits.add(a); } ( b = lit() { lits.add(b); })* { return f.and(lits); } +} + +Formula lit() : { Formula formula, op; } +{ + ( op = lit() { formula = f.not(op); } + | formula = simp() + ) + { return formula; } +} + +Formula simp() : { Formula formula; } +{ + ( formula = comparison() + | formula = constant() + | formula = equiv() + ) + { return formula; } +} + +Formula comparison() : { + Formula formula; + Pair, List> e; + CType c; + Token t; +} +{ + ( LOOKAHEAD(2) e = add() c = comperator() t = {formula = f.pbc(c, Integer.parseInt(t.image), e.first(), e.second()); } + | t = { formula = (t.image.startsWith("~") ? f.literal(t.image.substring(1), false) : f.literal(t.image, true)); } + | t = { formula = (t.image.startsWith("~") ? f.literal(t.image.substring(1), false) : f.literal(t.image, true)); } + ) + { return formula; } +} + +CType comperator() : { + +} +{ + { return CType.EQ; } + | { return CType.LE; } + | { return CType.LT; } + | { return CType.GE; } + | { return CType.GT; } +} + +Pair, List> add() : { + Pair m1, m2; + List lits = new ArrayList<>(); + List coeffs = new ArrayList<>(); + Token a; +} +{ + m1 = mul() { lits.add(m1.first()); coeffs.add(m1.second()); } (a = m2 = mul() { lits.add(m2.first()); coeffs.add (a.image.equals("+") ? m2.second() : -m2.second()); })* + { return new Pair<>(lits, coeffs); } +} + +Pair mul() : { + Token n, l; + Literal lit; + int c = 1; +} +{ + ( LOOKAHEAD(3) n = l = {lit = (l.image.startsWith("~") ? f.literal(l.image.substring(1), false) : f .literal(l.image, true)); c = Integer.parseInt(n.image); } + | LOOKAHEAD(3) n = l = {lit = f.literal(l.image, true); c = Integer.parseInt(n.image); } + | l = { lit = (l.image.startsWith("~") ? f.literal(l.image.substring(1), false) : f.literal (l.image, true) ); } + | n = { lit = f.literal(n.image, true); } + ) + { return new Pair<>(lit, c); } +} + +Formula constant() : {} +{ + { return f.verum(); } + | { return f.falsum(); } +} + diff --git a/src/main/java/com/booleworks/logicng/io/parsers/javacc/ParseException.java b/src/main/java/com/booleworks/logicng/io/parsers/javacc/ParseException.java new file mode 100644 index 00000000..96d3e14f --- /dev/null +++ b/src/main/java/com/booleworks/logicng/io/parsers/javacc/ParseException.java @@ -0,0 +1,195 @@ +/* Generated By:JavaCC: Do not edit this line. ParseException.java Version 7.0 */ +/* JavaCCOptions:KEEP_LINE_COLUMN=true */ +package com.booleworks.logicng.io.parsers.javacc; + +/** + * This exception is thrown when parse errors are encountered. + * You can explicitly create objects of this exception type by + * calling the method generateParseException in the generated + * parser. + * + * You can modify this class to customize your error reporting + * mechanisms so long as you retain the public fields. + */ +public class ParseException extends Exception { + + /** + * The version identifier for this Serializable class. + * Increment only if the serialized form of the + * class changes. + */ + private static final long serialVersionUID = 1L; + + /** + * The end of line string for this machine. + */ + protected static String EOL = System.getProperty("line.separator", "\n"); + + /** + * This constructor is used by the method "generateParseException" + * in the generated parser. Calling this constructor generates + * a new object of this type with the fields "currentToken", + * "expectedTokenSequences", and "tokenImage" set. + */ + public ParseException(Token currentTokenVal, + int[][] expectedTokenSequencesVal, + String[] tokenImageVal + ) + { + super(initialise(currentTokenVal, expectedTokenSequencesVal, tokenImageVal)); + currentToken = currentTokenVal; + expectedTokenSequences = expectedTokenSequencesVal; + tokenImage = tokenImageVal; + } + + /** + * The following constructors are for use by you for whatever + * purpose you can think of. Constructing the exception in this + * manner makes the exception behave in the normal way - i.e., as + * documented in the class "Throwable". The fields "errorToken", + * "expectedTokenSequences", and "tokenImage" do not contain + * relevant information. The JavaCC generated code does not use + * these constructors. + */ + + public ParseException() { + super(); + } + + /** Constructor with message. */ + public ParseException(String message) { + super(message); + } + + + /** + * This is the last token that has been consumed successfully. If + * this object has been created due to a parse error, the token + * following this token will (therefore) be the first error token. + */ + public Token currentToken; + + /** + * Each entry in this array is an array of integers. Each array + * of integers represents a sequence of tokens (by their ordinal + * values) that is expected at this point of the parse. + */ + public int[][] expectedTokenSequences; + + /** + * This is a reference to the "tokenImage" array of the generated + * parser within which the parse error occurred. This array is + * defined in the generated ...Constants interface. + */ + public String[] tokenImage; + + /** + * It uses "currentToken" and "expectedTokenSequences" to generate a parse + * error message and returns it. If this object has been created + * due to a parse error, and you do not catch it (it gets thrown + * from the parser) the correct error message + * gets displayed. + */ + private static String initialise(Token currentToken, + int[][] expectedTokenSequences, + String[] tokenImage) { + + StringBuilder expected = new StringBuilder(); + int maxSize = 0; + for (int i = 0; i < expectedTokenSequences.length; i++) { + if (maxSize < expectedTokenSequences[i].length) { + maxSize = expectedTokenSequences[i].length; + } + for (int j = 0; j < expectedTokenSequences[i].length; j++) { + expected.append(tokenImage[expectedTokenSequences[i][j]]).append(' '); + } + if (expectedTokenSequences[i][expectedTokenSequences[i].length - 1] != 0) { + expected.append("..."); + } + expected.append(EOL).append(" "); + } + String retval = "Encountered \""; + Token tok = currentToken.next; + for (int i = 0; i < maxSize; i++) { + if (i != 0) retval += " "; + if (tok.kind == 0) { + retval += tokenImage[0]; + break; + } + retval += " " + tokenImage[tok.kind]; + retval += " \""; + retval += add_escapes(tok.image); + retval += " \""; + tok = tok.next; + } + if (currentToken.next != null) { + retval += "\" at line " + currentToken.next.beginLine + ", column " + currentToken.next.beginColumn; + } + retval += "." + EOL; + + + if (expectedTokenSequences.length == 0) { + // Nothing to add here + } else { + if (expectedTokenSequences.length == 1) { + retval += "Was expecting:" + EOL + " "; + } else { + retval += "Was expecting one of:" + EOL + " "; + } + retval += expected.toString(); + } + + return retval; + } + + + /** + * Used to convert raw characters to their escaped version + * when these raw version cannot be used as part of an ASCII + * string literal. + */ + static String add_escapes(String str) { + StringBuilder retval = new StringBuilder(); + char ch; + for (int i = 0; i < str.length(); i++) { + switch (str.charAt(i)) + { + case '\b': + retval.append("\\b"); + continue; + case '\t': + retval.append("\\t"); + continue; + case '\n': + retval.append("\\n"); + continue; + case '\f': + retval.append("\\f"); + continue; + case '\r': + retval.append("\\r"); + continue; + case '\"': + retval.append("\\\""); + continue; + case '\'': + retval.append("\\\'"); + continue; + case '\\': + retval.append("\\\\"); + continue; + default: + if ((ch = str.charAt(i)) < 0x20 || ch > 0x7e) { + String s = "0000" + Integer.toString(ch, 16); + retval.append("\\u" + s.substring(s.length() - 4, s.length())); + } else { + retval.append(ch); + } + continue; + } + } + return retval.toString(); + } + +} +/* JavaCC - OriginalChecksum=46f01db80cc2a078b14401250f46b293 (do not edit this line) */ diff --git a/src/main/java/com/booleworks/logicng/io/parsers/javacc/SimpleCharStream.java b/src/main/java/com/booleworks/logicng/io/parsers/javacc/SimpleCharStream.java new file mode 100644 index 00000000..2828d690 --- /dev/null +++ b/src/main/java/com/booleworks/logicng/io/parsers/javacc/SimpleCharStream.java @@ -0,0 +1,472 @@ +/* Generated By:JavaCC: Do not edit this line. SimpleCharStream.java Version 7.0 */ +/* JavaCCOptions:STATIC=false,SUPPORT_CLASS_VISIBILITY_PUBLIC=true */ +package com.booleworks.logicng.io.parsers.javacc; + +/** + * An implementation of interface CharStream, where the stream is assumed to + * contain only ASCII characters (without unicode processing). + */ + +public class SimpleCharStream +{ +/** Whether parser is static. */ + public static final boolean staticFlag = false; + int bufsize; + int available; + int tokenBegin; +/** Position in buffer. */ + public int bufpos = -1; + protected int bufline[]; + protected int bufcolumn[]; + + protected int column = 0; + protected int line = 1; + + protected boolean prevCharIsCR = false; + protected boolean prevCharIsLF = false; + + protected java.io.Reader inputStream; + + protected char[] buffer; + protected int maxNextCharInd = 0; + protected int inBuf = 0; + protected int tabSize = 1; + protected boolean trackLineColumn = true; + + public void setTabSize(int i) { tabSize = i; } + public int getTabSize() { return tabSize; } + + + + protected void ExpandBuff(boolean wrapAround) + { + char[] newbuffer = new char[bufsize + 2048]; + int newbufline[] = new int[bufsize + 2048]; + int newbufcolumn[] = new int[bufsize + 2048]; + + try + { + if (wrapAround) + { + System.arraycopy(buffer, tokenBegin, newbuffer, 0, bufsize - tokenBegin); + System.arraycopy(buffer, 0, newbuffer, bufsize - tokenBegin, bufpos); + buffer = newbuffer; + + System.arraycopy(bufline, tokenBegin, newbufline, 0, bufsize - tokenBegin); + System.arraycopy(bufline, 0, newbufline, bufsize - tokenBegin, bufpos); + bufline = newbufline; + + System.arraycopy(bufcolumn, tokenBegin, newbufcolumn, 0, bufsize - tokenBegin); + System.arraycopy(bufcolumn, 0, newbufcolumn, bufsize - tokenBegin, bufpos); + bufcolumn = newbufcolumn; + + maxNextCharInd = (bufpos += (bufsize - tokenBegin)); + } + else + { + System.arraycopy(buffer, tokenBegin, newbuffer, 0, bufsize - tokenBegin); + buffer = newbuffer; + + System.arraycopy(bufline, tokenBegin, newbufline, 0, bufsize - tokenBegin); + bufline = newbufline; + + System.arraycopy(bufcolumn, tokenBegin, newbufcolumn, 0, bufsize - tokenBegin); + bufcolumn = newbufcolumn; + + maxNextCharInd = (bufpos -= tokenBegin); + } + } + catch (Throwable t) + { + throw new Error(t.getMessage()); + } + + + bufsize += 2048; + available = bufsize; + tokenBegin = 0; + } + + protected void FillBuff() throws java.io.IOException + { + if (maxNextCharInd == available) + { + if (available == bufsize) + { + if (tokenBegin > 2048) + { + bufpos = maxNextCharInd = 0; + available = tokenBegin; + } + else if (tokenBegin < 0) + bufpos = maxNextCharInd = 0; + else + ExpandBuff(false); + } + else if (available > tokenBegin) + available = bufsize; + else if ((tokenBegin - available) < 2048) + ExpandBuff(true); + else + available = tokenBegin; + } + + int i; + try { + if ((i = inputStream.read(buffer, maxNextCharInd, available - maxNextCharInd)) == -1) + { + inputStream.close(); + throw new java.io.IOException(); + } + else + maxNextCharInd += i; + return; + } + catch(java.io.IOException e) { + --bufpos; + backup(0); + if (tokenBegin == -1) + tokenBegin = bufpos; + throw e; + } + } + +/** Start. */ + public char BeginToken() throws java.io.IOException + { + tokenBegin = -1; + char c = readChar(); + tokenBegin = bufpos; + + return c; + } + + protected void UpdateLineColumn(char c) + { + column++; + + if (prevCharIsLF) + { + prevCharIsLF = false; + line += (column = 1); + } + else if (prevCharIsCR) + { + prevCharIsCR = false; + if (c == '\n') + { + prevCharIsLF = true; + } + else + line += (column = 1); + } + + switch (c) + { + case '\r' : + prevCharIsCR = true; + break; + case '\n' : + prevCharIsLF = true; + break; + case '\t' : + column--; + column += (tabSize - (column % tabSize)); + break; + default : + break; + } + + bufline[bufpos] = line; + bufcolumn[bufpos] = column; + } + +/** Read a character. */ + public char readChar() throws java.io.IOException + { + if (inBuf > 0) + { + --inBuf; + + if (++bufpos == bufsize) + bufpos = 0; + + return buffer[bufpos]; + } + + if (++bufpos >= maxNextCharInd) + FillBuff(); + + char c = buffer[bufpos]; + + UpdateLineColumn(c); + return c; + } + + /** + * @deprecated + * @see #getEndColumn + */ + @Deprecated + public int getColumn() { + return bufcolumn[bufpos]; + } + + /** + * @deprecated + * @see #getEndLine + */ + @Deprecated + public int getLine() { + return bufline[bufpos]; + } + + /** Get token end column number. */ + public int getEndColumn() { + return bufcolumn[bufpos]; + } + + /** Get token end line number. */ + public int getEndLine() { + return bufline[bufpos]; + } + + /** Get token beginning column number. */ + public int getBeginColumn() { + return bufcolumn[tokenBegin]; + } + + /** Get token beginning line number. */ + public int getBeginLine() { + return bufline[tokenBegin]; + } + +/** Backup a number of characters. */ + public void backup(int amount) { + + inBuf += amount; + if ((bufpos -= amount) < 0) + bufpos += bufsize; + } + + /** Constructor. */ + public SimpleCharStream(java.io.Reader dstream, int startline, + int startcolumn, int buffersize) + { + inputStream = dstream; + line = startline; + column = startcolumn - 1; + + available = bufsize = buffersize; + buffer = new char[buffersize]; + bufline = new int[buffersize]; + bufcolumn = new int[buffersize]; + } + + /** Constructor. */ + public SimpleCharStream(java.io.Reader dstream, int startline, + int startcolumn) + { + this(dstream, startline, startcolumn, 4096); + } + + /** Constructor. */ + public SimpleCharStream(java.io.Reader dstream) + { + this(dstream, 1, 1, 4096); + } + + /** Reinitialise. */ + public void ReInit(java.io.Reader dstream, int startline, + int startcolumn, int buffersize) + { + inputStream = dstream; + line = startline; + column = startcolumn - 1; + + if (buffer == null || buffersize != buffer.length) + { + available = bufsize = buffersize; + buffer = new char[buffersize]; + bufline = new int[buffersize]; + bufcolumn = new int[buffersize]; + } + prevCharIsLF = prevCharIsCR = false; + tokenBegin = inBuf = maxNextCharInd = 0; + bufpos = -1; + } + + /** Reinitialise. */ + public void ReInit(java.io.Reader dstream, int startline, + int startcolumn) + { + ReInit(dstream, startline, startcolumn, 4096); + } + + /** Reinitialise. */ + public void ReInit(java.io.Reader dstream) + { + ReInit(dstream, 1, 1, 4096); + } + /** Constructor. */ + public SimpleCharStream(java.io.InputStream dstream, String encoding, int startline, + int startcolumn, int buffersize) throws java.io.UnsupportedEncodingException + { + this(encoding == null ? new java.io.InputStreamReader(dstream) : new java.io.InputStreamReader(dstream, encoding), startline, startcolumn, buffersize); + } + + /** Constructor. */ + public SimpleCharStream(java.io.InputStream dstream, int startline, + int startcolumn, int buffersize) + { + this(new java.io.InputStreamReader(dstream), startline, startcolumn, buffersize); + } + + /** Constructor. */ + public SimpleCharStream(java.io.InputStream dstream, String encoding, int startline, + int startcolumn) throws java.io.UnsupportedEncodingException + { + this(dstream, encoding, startline, startcolumn, 4096); + } + + /** Constructor. */ + public SimpleCharStream(java.io.InputStream dstream, int startline, + int startcolumn) + { + this(dstream, startline, startcolumn, 4096); + } + + /** Constructor. */ + public SimpleCharStream(java.io.InputStream dstream, String encoding) throws java.io.UnsupportedEncodingException + { + this(dstream, encoding, 1, 1, 4096); + } + + /** Constructor. */ + public SimpleCharStream(java.io.InputStream dstream) + { + this(dstream, 1, 1, 4096); + } + + /** Reinitialise. */ + public void ReInit(java.io.InputStream dstream, String encoding, int startline, + int startcolumn, int buffersize) throws java.io.UnsupportedEncodingException + { + ReInit(encoding == null ? new java.io.InputStreamReader(dstream) : new java.io.InputStreamReader(dstream, encoding), startline, startcolumn, buffersize); + } + + /** Reinitialise. */ + public void ReInit(java.io.InputStream dstream, int startline, + int startcolumn, int buffersize) + { + ReInit(new java.io.InputStreamReader(dstream), startline, startcolumn, buffersize); + } + + /** Reinitialise. */ + public void ReInit(java.io.InputStream dstream, String encoding) throws java.io.UnsupportedEncodingException + { + ReInit(dstream, encoding, 1, 1, 4096); + } + + /** Reinitialise. */ + public void ReInit(java.io.InputStream dstream) + { + ReInit(dstream, 1, 1, 4096); + } + /** Reinitialise. */ + public void ReInit(java.io.InputStream dstream, String encoding, int startline, + int startcolumn) throws java.io.UnsupportedEncodingException + { + ReInit(dstream, encoding, startline, startcolumn, 4096); + } + /** Reinitialise. */ + public void ReInit(java.io.InputStream dstream, int startline, + int startcolumn) + { + ReInit(dstream, startline, startcolumn, 4096); + } + /** Get token literal value. */ + public String GetImage() + { + if (bufpos >= tokenBegin) + return new String(buffer, tokenBegin, bufpos - tokenBegin + 1); + else + return new String(buffer, tokenBegin, bufsize - tokenBegin) + + new String(buffer, 0, bufpos + 1); + } + + /** Get the suffix. */ + public char[] GetSuffix(int len) + { + char[] ret = new char[len]; + + if ((bufpos + 1) >= len) + System.arraycopy(buffer, bufpos - len + 1, ret, 0, len); + else + { + System.arraycopy(buffer, bufsize - (len - bufpos - 1), ret, 0, + len - bufpos - 1); + System.arraycopy(buffer, 0, ret, len - bufpos - 1, bufpos + 1); + } + + return ret; + } + + /** Reset buffer when finished. */ + public void Done() + { + buffer = null; + bufline = null; + bufcolumn = null; + } + + /** + * Method to adjust line and column numbers for the start of a token. + */ + public void adjustBeginLineColumn(int newLine, int newCol) + { + int start = tokenBegin; + int len; + + if (bufpos >= tokenBegin) + { + len = bufpos - tokenBegin + inBuf + 1; + } + else + { + len = bufsize - tokenBegin + bufpos + 1 + inBuf; + } + + int i = 0, j = 0, k = 0; + int nextColDiff = 0, columnDiff = 0; + + while (i < len && bufline[j = start % bufsize] == bufline[k = ++start % bufsize]) + { + bufline[j] = newLine; + nextColDiff = columnDiff + bufcolumn[k] - bufcolumn[j]; + bufcolumn[j] = newCol + columnDiff; + columnDiff = nextColDiff; + i++; + } + + if (i < len) + { + bufline[j] = newLine++; + bufcolumn[j] = newCol + columnDiff; + + while (i++ < len) + { + if (bufline[j = start % bufsize] != bufline[++start % bufsize]) + bufline[j] = newLine++; + else + bufline[j] = newLine; + } + } + + line = bufline[j]; + column = bufcolumn[j]; + } + boolean getTrackLineColumn() { return trackLineColumn; } + void setTrackLineColumn(boolean tlc) { trackLineColumn = tlc; } +} +/* JavaCC - OriginalChecksum=7754e5c0e449afa54d1e66b9201514e6 (do not edit this line) */ diff --git a/src/main/java/com/booleworks/logicng/io/parsers/javacc/Token.java b/src/main/java/com/booleworks/logicng/io/parsers/javacc/Token.java new file mode 100644 index 00000000..02953ebe --- /dev/null +++ b/src/main/java/com/booleworks/logicng/io/parsers/javacc/Token.java @@ -0,0 +1,132 @@ +/* Generated By:JavaCC: Do not edit this line. Token.java Version 7.0 */ +/* JavaCCOptions:TOKEN_EXTENDS=,KEEP_LINE_COLUMN=true,SUPPORT_CLASS_VISIBILITY_PUBLIC=true */ +package com.booleworks.logicng.io.parsers.javacc; + +/** + * Describes the input token stream. + */ + +public class Token implements java.io.Serializable { + + /** + * The version identifier for this Serializable class. + * Increment only if the serialized form of the + * class changes. + */ + private static final long serialVersionUID = 1L; + + /** + * An integer that describes the kind of this token. This numbering + * system is determined by JavaCCParser, and a table of these numbers is + * stored in the file ...Constants.java. + */ + public int kind; + + /** The line number of the first character of this Token. */ + public int beginLine; + /** The column number of the first character of this Token. */ + public int beginColumn; + /** The line number of the last character of this Token. */ + public int endLine; + /** The column number of the last character of this Token. */ + public int endColumn; + + /** + * The string image of the token. + */ + public String image; + + /** + * A reference to the next regular (non-special) token from the input + * stream. If this is the last token from the input stream, or if the + * token manager has not read tokens beyond this one, this field is + * set to null. This is true only if this token is also a regular + * token. Otherwise, see below for a description of the contents of + * this field. + */ + public Token next; + + /** + * This field is used to access special tokens that occur prior to this + * token, but after the immediately preceding regular (non-special) token. + * If there are no such special tokens, this field is set to null. + * When there are more than one such special token, this field refers + * to the last of these special tokens, which in turn refers to the next + * previous special token through its specialToken field, and so on + * until the first special token (whose specialToken field is null). + * The next fields of special tokens refer to other special tokens that + * immediately follow it (without an intervening regular token). If there + * is no such token, this field is null. + */ + public Token specialToken; + + /** + * An optional attribute value of the Token. + * Tokens which are not used as syntactic sugar will often contain + * meaningful values that will be used later on by the compiler or + * interpreter. This attribute value is often different from the image. + * Any subclass of Token that actually wants to return a non-null value can + * override this method as appropriate. + */ + public Object getValue() { + return null; + } + + /** + * No-argument constructor + */ + public Token() {} + + /** + * Constructs a new token for the specified Image. + */ + public Token(int kind) + { + this(kind, null); + } + + /** + * Constructs a new token for the specified Image and Kind. + */ + public Token(int kind, String image) + { + this.kind = kind; + this.image = image; + } + + /** + * Returns the image. + */ + @Override + public String toString() + { + return image; + } + + /** + * Returns a new Token object, by default. However, if you want, you + * can create and return subclass objects based on the value of ofKind. + * Simply add the cases to the switch for all those special cases. + * For example, if you have a subclass of Token called IDToken that + * you want to create if ofKind is ID, simply add something like : + * + * case MyParserConstants.ID : return new IDToken(ofKind, image); + * + * to the following switch statement. Then you can cast matchedToken + * variable to the appropriate type and use sit in your lexical actions. + */ + public static Token newToken(int ofKind, String image) + { + switch(ofKind) + { + default : return new Token(ofKind, image); + } + } + + public static Token newToken(int ofKind) + { + return newToken(ofKind, null); + } + +} +/* JavaCC - OriginalChecksum=6ce50ba5b27fbb845f54c77bde9b8a44 (do not edit this line) */ diff --git a/src/main/java/com/booleworks/logicng/io/parsers/javacc/TokenMgrError.java b/src/main/java/com/booleworks/logicng/io/parsers/javacc/TokenMgrError.java new file mode 100644 index 00000000..9c26264c --- /dev/null +++ b/src/main/java/com/booleworks/logicng/io/parsers/javacc/TokenMgrError.java @@ -0,0 +1,148 @@ +/* Generated By:JavaCC: Do not edit this line. TokenMgrError.java Version 7.0 */ +/* JavaCCOptions: */ +package com.booleworks.logicng.io.parsers.javacc; + +/** Token Manager Error. */ +@SuppressWarnings("all") +public class TokenMgrError extends Error +{ + + /** + * The version identifier for this Serializable class. + * Increment only if the serialized form of the + * class changes. + */ + private static final long serialVersionUID = 1L; + + /* + * Ordinals for various reasons why an Error of this type can be thrown. + */ + + /** + * Lexical error occurred. + */ + public static final int LEXICAL_ERROR = 0; + + /** + * An attempt was made to create a second instance of a static token manager. + */ + public static final int STATIC_LEXER_ERROR = 1; + + /** + * Tried to change to an invalid lexical state. + */ + public static final int INVALID_LEXICAL_STATE = 2; + + /** + * Detected (and bailed out of) an infinite loop in the token manager. + */ + public static final int LOOP_DETECTED = 3; + + /** + * Indicates the reason why the exception is thrown. It will have + * one of the above 4 values. + */ + int errorCode; + + /** + * Replaces unprintable characters by their escaped (or unicode escaped) + * equivalents in the given string + */ + protected static final String addEscapes(String str) { + StringBuilder retval = new StringBuilder(); + char ch; + for (int i = 0; i < str.length(); i++) { + switch (str.charAt(i)) + { + case '\b': + retval.append("\\b"); + continue; + case '\t': + retval.append("\\t"); + continue; + case '\n': + retval.append("\\n"); + continue; + case '\f': + retval.append("\\f"); + continue; + case '\r': + retval.append("\\r"); + continue; + case '\"': + retval.append("\\\""); + continue; + case '\'': + retval.append("\\\'"); + continue; + case '\\': + retval.append("\\\\"); + continue; + default: + if ((ch = str.charAt(i)) < 0x20 || ch > 0x7e) { + String s = "0000" + Integer.toString(ch, 16); + retval.append("\\u" + s.substring(s.length() - 4, s.length())); + } else { + retval.append(ch); + } + continue; + } + } + return retval.toString(); + } + + /** + * Returns a detailed message for the Error when it is thrown by the + * token manager to indicate a lexical error. + * Parameters : + * EOFSeen : indicates if EOF caused the lexical error + * lexState : lexical state in which this error occurred + * errorLine : line number when the error occurred + * errorColumn : column number when the error occurred + * errorAfter : prefix that was seen before this error occurred + * curchar : the offending character + * Note: You can customize the lexical error message by modifying this method. + */ + protected static String LexicalErr(boolean EOFSeen, int lexState, int errorLine, int errorColumn, String errorAfter, int curChar) { + return("Lexical error at line " + // + errorLine + ", column " + // + errorColumn + ". Encountered: " + // + (EOFSeen ? "" : ("'" + addEscapes(String.valueOf((char) curChar)) + "' (" + curChar + "),")) + // + (errorAfter == null || errorAfter.length() == 0 ? "" : " after prefix \"" + addEscapes(errorAfter) + "\"")) + // + (lexState == 0 ? "" : " (in lexical state " + lexState + ")"); + } + + /** + * You can also modify the body of this method to customize your error messages. + * For example, cases like LOOP_DETECTED and INVALID_LEXICAL_STATE are not + * of end-users concern, so you can return something like : + * + * "Internal Error : Please file a bug report .... " + * + * from this method for such cases in the release version of your parser. + */ + @Override + public String getMessage() { + return super.getMessage(); + } + + /* + * Constructors of various flavors follow. + */ + + /** No arg constructor. */ + public TokenMgrError() { + } + + /** Constructor with message and reason. */ + public TokenMgrError(String message, int reason) { + super(message); + errorCode = reason; + } + + /** Full Constructor. */ + public TokenMgrError(boolean EOFSeen, int lexState, int errorLine, int errorColumn, String errorAfter, int curChar, int reason) { + this(LexicalErr(EOFSeen, lexState, errorLine, errorColumn, errorAfter, curChar), reason); + } +} +/* JavaCC - OriginalChecksum=6858ce64d9a42d203e099fe08e63c4f0 (do not edit this line) */ diff --git a/src/test/java/com/booleworks/logicng/io/parsers/PropositionalParserTest.java b/src/test/java/com/booleworks/logicng/io/parsers/PropositionalParserTest.java index c8919648..8214b95d 100644 --- a/src/test/java/com/booleworks/logicng/io/parsers/PropositionalParserTest.java +++ b/src/test/java/com/booleworks/logicng/io/parsers/PropositionalParserTest.java @@ -15,25 +15,31 @@ import org.assertj.core.api.Assertions; import org.junit.jupiter.api.Test; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.List; + public class PropositionalParserTest extends TestWithExampleFormulas { @Test public void testExceptions() throws ParserException { - final PropositionalParser parser = new PropositionalParser(f); + final PropositionalParserNew parser = new PropositionalParserNew(f); Assertions.assertThat(parser.parse("")).isEqualTo(f.verum()); Assertions.assertThat(parser.parse((String) null)).isEqualTo(f.verum()); } @Test public void testParseConstants() throws ParserException { - final PropositionalParser parser = new PropositionalParser(f); + final PropositionalParserNew parser = new PropositionalParserNew(f); Assertions.assertThat(parser.parse("$true")).isEqualTo(f.verum()); Assertions.assertThat(parser.parse("$false")).isEqualTo(f.falsum()); } @Test public void testParseLiterals() throws ParserException { - final PropositionalParser parser = new PropositionalParser(f); + final PropositionalParserNew parser = new PropositionalParserNew(f); Assertions.assertThat(parser.parse("A")).isEqualTo(f.variable("A")); Assertions.assertThat(parser.parse("a")).isEqualTo(f.variable("a")); Assertions.assertThat(parser.parse("a1")).isEqualTo(f.variable("a1")); @@ -52,7 +58,7 @@ public void testParseLiterals() throws ParserException { @Test public void testParseOperators() throws ParserException { - final PropositionalParser parser = new PropositionalParser(f); + final PropositionalParserNew parser = new PropositionalParserNew(f); Assertions.assertThat(parser.parse("~a")).isEqualTo(f.not(f.variable("a"))); Assertions.assertThat(parser.parse("~Var")).isEqualTo(f.not(f.variable("Var"))); Assertions.assertThat(parser.parse("a & b")).isEqualTo(f.and(f.variable("a"), f.variable("b"))); @@ -73,7 +79,7 @@ public void testParseOperators() throws ParserException { @Test public void testParseMultiplication() throws ParserException { - final PropositionalParser parser = new PropositionalParser(f); + final PropositionalParserNew parser = new PropositionalParserNew(f); Assertions.assertThat(parser.parse("13 * abc = 4")) .isEqualTo(f.pbc(CType.EQ, 4, new Literal[]{f.variable("abc")}, new int[]{13})); Assertions.assertThat(parser.parse("-13 * a = 4")) @@ -96,7 +102,7 @@ public void testParseMultiplication() throws ParserException { @Test public void testParseAddition() throws ParserException { - final PropositionalParser parser = new PropositionalParser(f); + final PropositionalParserNew parser = new PropositionalParserNew(f); Assertions.assertThat(parser.parse("4 * c + -4 * ~d < -4")).isEqualTo( f.pbc(CType.LT, -4, new Literal[]{f.variable("c"), f.literal("d", false)}, new int[]{4, -4})); Assertions.assertThat(parser.parse("5 * c + -5 * ~c >= -5")).isEqualTo( @@ -119,7 +125,7 @@ public void testParseAddition() throws ParserException { @Test public void testCombination() throws ParserException { - final PropositionalParser parser = new PropositionalParser(f); + final PropositionalParserNew parser = new PropositionalParserNew(f); final Formula pbc = f.pbc(CType.GT, -6, new Literal[]{f.variable("a"), f.literal("b", false), f.literal("c", false)}, new int[]{6, -6, 12}); Assertions.assertThat(parser.parse("(x => y & z) & (6 * a + -6 * ~b + 12 * ~c > -6)")) @@ -129,7 +135,7 @@ public void testCombination() throws ParserException { @Test public void testParsePrecedences() throws ParserException { - final PropositionalParser parser = new PropositionalParser(f); + final PropositionalParserNew parser = new PropositionalParserNew(f); Assertions.assertThat(parser.parse("x | y & z")) .isEqualTo(f.or(f.variable("x"), f.and(f.variable("y"), f.variable("z")))); Assertions.assertThat(parser.parse("x & y | z")) @@ -182,13 +188,13 @@ public void testParsePrecedences() throws ParserException { @Test public void parseEmptyString() throws ParserException { - final PropositionalParser parser = new PropositionalParser(f); + final PropositionalParserNew parser = new PropositionalParserNew(f); Assertions.assertThat(parser.parse("")).isEqualTo(f.verum()); } @Test public void testSkipSymbols() throws ParserException { - final PropositionalParser parser = new PropositionalParser(f); + final PropositionalParserNew parser = new PropositionalParserNew(f); Assertions.assertThat(parser.parse(" ")).isEqualTo(f.verum()); Assertions.assertThat(parser.parse("\t")).isEqualTo(f.verum()); Assertions.assertThat(parser.parse("\n")).isEqualTo(f.verum()); @@ -202,7 +208,7 @@ public void testSkipSymbols() throws ParserException { @Test public void testNumberLiterals() throws ParserException { final FormulaFactory f = FormulaFactory.caching(); - final PropositionalParser parser = new PropositionalParser(f); + final PropositionalParserNew parser = new PropositionalParserNew(f); Assertions.assertThat(parser.parse("12 & A")).isEqualTo(f.and(f.variable("12"), f.variable("A"))); Assertions.assertThat(parser.parse("~12 & A")).isEqualTo(f.and(f.literal("12", false), f.variable("A"))); Assertions.assertThat(parser.parse("12 * 12 + 13 * A + 10 * B <= 25")).isEqualTo(f.pbc(CType.LE, 25, @@ -219,89 +225,148 @@ public void testFormulaFactoryParser() throws ParserException { @Test public void testIllegalVariable1() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("$$%")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("$$%")).isInstanceOf(ParserException.class); } @Test public void testIllegalVariable3() { - assertThatThrownBy(() -> new PropositionalParser(f).parse(";;23")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse(";;23")).isInstanceOf(ParserException.class); } @Test public void testIllegalVariable4() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("{0}")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("{0}")).isInstanceOf(ParserException.class); } @Test public void testIllegalOperator1() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("A + B")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("A + B")).isInstanceOf(ParserException.class); } @Test public void testIllegalOperator2() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("A &")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("A &")).isInstanceOf(ParserException.class); } @Test public void testIllegalOperator3() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("A /")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("A /")).isInstanceOf(ParserException.class); } @Test public void testIllegalOperator4() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("-A")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("-A")).isInstanceOf(ParserException.class); } @Test public void testIllegalOperator5() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("A * B")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("A * B")).isInstanceOf(ParserException.class); } @Test public void testIllegalBrackets1() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("(A & B")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("(A & B")).isInstanceOf(ParserException.class); } @Test public void testIllegalFormula1() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("((A & B)")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("((A & B)")).isInstanceOf(ParserException.class); } @Test public void testIllegalFormula2() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("(A & (C & D) B)")) + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("(A & (C & D) B)")) .isInstanceOf(ParserException.class); } @Test public void testIllegalFormula3() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("A | A + (C | B + C)")) + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("A | A + (C | B + C)")) .isInstanceOf(ParserException.class); } @Test public void testIllegalFormula4() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("A | A & (C | B & C")) + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("A | A & (C | B & C")) .isInstanceOf(ParserException.class); } @Test public void testIllegalFormula5() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("A & ~B)")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("A & ~B)")).isInstanceOf(ParserException.class); } @Test public void testIllegalFormula6() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("12)")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("12)")).isInstanceOf(ParserException.class); } @Test public void testIllegalFormula7() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("ab@cd)")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("ab@cd)")).isInstanceOf(ParserException.class); } @Test public void testIllegalSkipPosition() { - assertThatThrownBy(() -> new PropositionalParser(f).parse("- 1*x <= 3")).isInstanceOf(ParserException.class); + assertThatThrownBy(() -> new PropositionalParserNew(f).parse("- 1*x <= 3")).isInstanceOf(ParserException.class); + } + + @Test + public void parseLargeFormula() throws ParserException, IOException { + final int num = 100; + long sumOld = 0; + long sumNew = 0; + final String input = Files.readString(Paths.get("src/test/resources/formulas/large_formula.txt")); + for (int i = 0; i < num; i++) { + final FormulaFactory f1 = FormulaFactory.caching(); + final var t1 = System.currentTimeMillis(); + final Formula formula1 = new PropositionalParser(f1).parse(input); + final var t2 = System.currentTimeMillis(); + sumOld += t2 - t1; + + final FormulaFactory f2 = FormulaFactory.caching(); + final var t3 = System.currentTimeMillis(); + final Formula formula2 = new PropositionalParserNew(f2).parse(input); + final var t4 = System.currentTimeMillis(); + sumNew += t4 - t3; + + assertThat(formula1.equals(formula2)).isTrue(); + } + System.out.println("ANTLR: " + (sumOld / num) + " ms."); + System.out.println("JavaCC: " + (sumNew / num) + " ms."); + } + + @Test + public void parseLargeFormulas() throws ParserException, IOException { + final int num = 20; + long sumOld = 0; + long sumNew = 0; + final List input = Files.readAllLines(Paths.get("src/test/resources/formulas/formula3.txt")); + for (int i = 0; i < num; i++) { + final FormulaFactory f1 = FormulaFactory.caching(); + final var p1 = new PropositionalParser(f1); + final var t1 = System.currentTimeMillis(); + final List formula1 = new ArrayList<>(); + for (final String s : input) { + formula1.add(p1.parse(s)); + } + + final var t2 = System.currentTimeMillis(); + sumOld += t2 - t1; + + final FormulaFactory f2 = FormulaFactory.caching(); + final var p2 = new PropositionalParserNew(f2); + final var t3 = System.currentTimeMillis(); + final List formula2 = new ArrayList<>(); + for (final String s : input) { + formula2.add(p2.parse(s)); + } + final var t4 = System.currentTimeMillis(); + sumNew += t4 - t3; + + //assertThat(formula1.equals(formula2)).isTrue(); + } + System.out.println("ANTLR: " + (sumOld / num) + " ms."); + System.out.println("JavaCC: " + (sumNew / num) + " ms."); } }