ID() { return getTokens(RefinementsLanguageParser.ID); }
+ public TerminalNode ID(int i) {
+ return getToken(RefinementsLanguageParser.ID, i);
+ }
+ public TargetInvocationContext(LeafsContext ctx) { copyFrom(ctx); }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class LitGroupContext extends LeafsContext {
+ public LeafsContext leafs() {
+ return getRuleContext(LeafsContext.class,0);
+ }
+ public LitGroupContext(LeafsContext ctx) { copyFrom(ctx); }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class LitContext extends LeafsContext {
+ public LiteralContext literal() {
+ return getRuleContext(LiteralContext.class,0);
+ }
+ public LitContext(LeafsContext ctx) { copyFrom(ctx); }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class VarContext extends LeafsContext {
+ public TerminalNode ID() { return getToken(RefinementsLanguageParser.ID, 0); }
+ public VarContext(LeafsContext ctx) { copyFrom(ctx); }
+ }
+
+ public final LeafsContext leafs() throws RecognitionException {
+ LeafsContext _localctx = new LeafsContext(_ctx, getState());
+ enterRule(_localctx, 8, RULE_leafs);
+ try {
+ setState(80);
+ _errHandler.sync(this);
+ switch ( getInterpreter().adaptivePredict(_input,8,_ctx) ) {
+ case 1:
+ _localctx = new LitGroupContext(_localctx);
+ enterOuterAlt(_localctx, 1);
+ {
+ setState(71);
+ match(T__0);
+ setState(72);
+ leafs();
+ setState(73);
+ match(T__1);
+ }
+ break;
+ case 2:
+ _localctx = new LitContext(_localctx);
+ enterOuterAlt(_localctx, 2);
+ {
+ setState(75);
+ literal();
+ }
+ break;
+ case 3:
+ _localctx = new VarContext(_localctx);
+ enterOuterAlt(_localctx, 3);
+ {
+ setState(76);
+ match(ID);
+ }
+ break;
+ case 4:
+ _localctx = new TargetInvocationContext(_localctx);
+ enterOuterAlt(_localctx, 4);
+ {
+ setState(77);
+ match(ID);
+ setState(78);
+ match(T__4);
+ setState(79);
+ match(ID);
+ }
+ break;
+ }
+ }
+ catch (RecognitionException re) {
+ _localctx.exception = re;
+ _errHandler.reportError(this, re);
+ _errHandler.recover(this, re);
+ }
+ finally {
+ exitRule();
+ }
+ return _localctx;
+ }
+
+ @SuppressWarnings("CheckReturnValue")
+ public static class LiteralContext extends ParserRuleContext {
+ public LiteralContext(ParserRuleContext parent, int invokingState) {
+ super(parent, invokingState);
+ }
+ @Override public int getRuleIndex() { return RULE_literal; }
+
+ public LiteralContext() { }
+ public void copyFrom(LiteralContext ctx) {
+ super.copyFrom(ctx);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class LitIntContext extends LiteralContext {
+ public TerminalNode INT() { return getToken(RefinementsLanguageParser.INT, 0); }
+ public LitIntContext(LiteralContext ctx) { copyFrom(ctx); }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class LitBoolContext extends LiteralContext {
+ public TerminalNode BOOL() { return getToken(RefinementsLanguageParser.BOOL, 0); }
+ public LitBoolContext(LiteralContext ctx) { copyFrom(ctx); }
+ }
+
+ public final LiteralContext literal() throws RecognitionException {
+ LiteralContext _localctx = new LiteralContext(_ctx, getState());
+ enterRule(_localctx, 10, RULE_literal);
+ try {
+ setState(84);
+ _errHandler.sync(this);
+ switch (_input.LA(1)) {
+ case BOOL:
+ _localctx = new LitBoolContext(_localctx);
+ enterOuterAlt(_localctx, 1);
+ {
+ setState(82);
+ match(BOOL);
+ }
+ break;
+ case INT:
+ _localctx = new LitIntContext(_localctx);
+ enterOuterAlt(_localctx, 2);
+ {
+ setState(83);
+ match(INT);
+ }
+ break;
+ default:
+ throw new NoViableAltException(this);
+ }
+ }
+ catch (RecognitionException re) {
+ _localctx.exception = re;
+ _errHandler.reportError(this, re);
+ _errHandler.recover(this, re);
+ }
+ finally {
+ exitRule();
+ }
+ return _localctx;
+ }
+
+ public boolean sempred(RuleContext _localctx, int ruleIndex, int predIndex) {
+ switch (ruleIndex) {
+ case 1:
+ return pred_sempred((PredContext)_localctx, predIndex);
+ case 2:
+ return exp_sempred((ExpContext)_localctx, predIndex);
+ case 3:
+ return operand_sempred((OperandContext)_localctx, predIndex);
+ }
+ return true;
+ }
+ private boolean pred_sempred(PredContext _localctx, int predIndex) {
+ switch (predIndex) {
+ case 0:
+ return precpred(_ctx, 2);
+ }
+ return true;
+ }
+ private boolean exp_sempred(ExpContext _localctx, int predIndex) {
+ switch (predIndex) {
+ case 1:
+ return precpred(_ctx, 2);
+ }
+ return true;
+ }
+ private boolean operand_sempred(OperandContext _localctx, int predIndex) {
+ switch (predIndex) {
+ case 2:
+ return precpred(_ctx, 4);
+ case 3:
+ return precpred(_ctx, 3);
+ }
+ return true;
+ }
+
+ public static final String _serializedATN =
+ "\u0004\u0001\rW\u0002\u0000\u0007\u0000\u0002\u0001\u0007\u0001\u0002"+
+ "\u0002\u0007\u0002\u0002\u0003\u0007\u0003\u0002\u0004\u0007\u0004\u0002"+
+ "\u0005\u0007\u0005\u0001\u0000\u0001\u0000\u0003\u0000\u000f\b\u0000\u0001"+
+ "\u0001\u0001\u0001\u0001\u0001\u0001\u0001\u0001\u0001\u0001\u0001\u0001"+
+ "\u0001\u0001\u0001\u0003\u0001\u0019\b\u0001\u0001\u0001\u0001\u0001\u0001"+
+ "\u0001\u0005\u0001\u001e\b\u0001\n\u0001\f\u0001!\t\u0001\u0001\u0002"+
+ "\u0001\u0002\u0001\u0002\u0001\u0002\u0001\u0002\u0001\u0002\u0003\u0002"+
+ ")\b\u0002\u0001\u0002\u0001\u0002\u0001\u0002\u0005\u0002.\b\u0002\n\u0002"+
+ "\f\u00021\t\u0002\u0001\u0003\u0001\u0003\u0001\u0003\u0001\u0003\u0001"+
+ "\u0003\u0001\u0003\u0001\u0003\u0001\u0003\u0003\u0003;\b\u0003\u0001"+
+ "\u0003\u0001\u0003\u0001\u0003\u0001\u0003\u0001\u0003\u0001\u0003\u0005"+
+ "\u0003C\b\u0003\n\u0003\f\u0003F\t\u0003\u0001\u0004\u0001\u0004\u0001"+
+ "\u0004\u0001\u0004\u0001\u0004\u0001\u0004\u0001\u0004\u0001\u0004\u0001"+
+ "\u0004\u0003\u0004Q\b\u0004\u0001\u0005\u0001\u0005\u0003\u0005U\b\u0005"+
+ "\u0001\u0005\u0000\u0003\u0002\u0004\u0006\u0006\u0000\u0002\u0004\u0006"+
+ "\b\n\u0000\u0000^\u0000\u000e\u0001\u0000\u0000\u0000\u0002\u0018\u0001"+
+ "\u0000\u0000\u0000\u0004(\u0001\u0000\u0000\u0000\u0006:\u0001\u0000\u0000"+
+ "\u0000\bP\u0001\u0000\u0000\u0000\nT\u0001\u0000\u0000\u0000\f\u000f\u0003"+
+ "\u0002\u0001\u0000\r\u000f\u0001\u0000\u0000\u0000\u000e\f\u0001\u0000"+
+ "\u0000\u0000\u000e\r\u0001\u0000\u0000\u0000\u000f\u0001\u0001\u0000\u0000"+
+ "\u0000\u0010\u0011\u0006\u0001\uffff\uffff\u0000\u0011\u0012\u0005\u0001"+
+ "\u0000\u0000\u0012\u0013\u0003\u0002\u0001\u0000\u0013\u0014\u0005\u0002"+
+ "\u0000\u0000\u0014\u0019\u0001\u0000\u0000\u0000\u0015\u0016\u0005\u0003"+
+ "\u0000\u0000\u0016\u0019\u0003\u0002\u0001\u0003\u0017\u0019\u0003\u0004"+
+ "\u0002\u0000\u0018\u0010\u0001\u0000\u0000\u0000\u0018\u0015\u0001\u0000"+
+ "\u0000\u0000\u0018\u0017\u0001\u0000\u0000\u0000\u0019\u001f\u0001\u0000"+
+ "\u0000\u0000\u001a\u001b\n\u0002\u0000\u0000\u001b\u001c\u0005\u0006\u0000"+
+ "\u0000\u001c\u001e\u0003\u0002\u0001\u0003\u001d\u001a\u0001\u0000\u0000"+
+ "\u0000\u001e!\u0001\u0000\u0000\u0000\u001f\u001d\u0001\u0000\u0000\u0000"+
+ "\u001f \u0001\u0000\u0000\u0000 \u0003\u0001\u0000\u0000\u0000!\u001f"+
+ "\u0001\u0000\u0000\u0000\"#\u0006\u0002\uffff\uffff\u0000#$\u0005\u0001"+
+ "\u0000\u0000$%\u0003\u0004\u0002\u0000%&\u0005\u0002\u0000\u0000&)\u0001"+
+ "\u0000\u0000\u0000\')\u0003\u0006\u0003\u0000(\"\u0001\u0000\u0000\u0000"+
+ "(\'\u0001\u0000\u0000\u0000)/\u0001\u0000\u0000\u0000*+\n\u0002\u0000"+
+ "\u0000+,\u0005\u0007\u0000\u0000,.\u0003\u0004\u0002\u0003-*\u0001\u0000"+
+ "\u0000\u0000.1\u0001\u0000\u0000\u0000/-\u0001\u0000\u0000\u0000/0\u0001"+
+ "\u0000\u0000\u00000\u0005\u0001\u0000\u0000\u00001/\u0001\u0000\u0000"+
+ "\u000023\u0006\u0003\uffff\uffff\u00003;\u0003\b\u0004\u000045\u0005\u0003"+
+ "\u0000\u00005;\u0003\u0006\u0003\u000267\u0005\u0001\u0000\u000078\u0003"+
+ "\u0006\u0003\u000089\u0005\u0002\u0000\u00009;\u0001\u0000\u0000\u0000"+
+ ":2\u0001\u0000\u0000\u0000:4\u0001\u0000\u0000\u0000:6\u0001\u0000\u0000"+
+ "\u0000;D\u0001\u0000\u0000\u0000<=\n\u0004\u0000\u0000=>\u0005\b\u0000"+
+ "\u0000>C\u0003\u0006\u0003\u0005?@\n\u0003\u0000\u0000@A\u0005\u0004\u0000"+
+ "\u0000AC\u0003\u0006\u0003\u0004B<\u0001\u0000\u0000\u0000B?\u0001\u0000"+
+ "\u0000\u0000CF\u0001\u0000\u0000\u0000DB\u0001\u0000\u0000\u0000DE\u0001"+
+ "\u0000\u0000\u0000E\u0007\u0001\u0000\u0000\u0000FD\u0001\u0000\u0000"+
+ "\u0000GH\u0005\u0001\u0000\u0000HI\u0003\b\u0004\u0000IJ\u0005\u0002\u0000"+
+ "\u0000JQ\u0001\u0000\u0000\u0000KQ\u0003\n\u0005\u0000LQ\u0005\u000b\u0000"+
+ "\u0000MN\u0005\u000b\u0000\u0000NO\u0005\u0005\u0000\u0000OQ\u0005\u000b"+
+ "\u0000\u0000PG\u0001\u0000\u0000\u0000PK\u0001\u0000\u0000\u0000PL\u0001"+
+ "\u0000\u0000\u0000PM\u0001\u0000\u0000\u0000Q\t\u0001\u0000\u0000\u0000"+
+ "RU\u0005\t\u0000\u0000SU\u0005\f\u0000\u0000TR\u0001\u0000\u0000\u0000"+
+ "TS\u0001\u0000\u0000\u0000U\u000b\u0001\u0000\u0000\u0000\n\u000e\u0018"+
+ "\u001f(/:BDPT";
+ public static final ATN _ATN =
+ new ATNDeserializer().deserialize(_serializedATN.toCharArray());
+ static {
+ _decisionToDFA = new DFA[_ATN.getNumberOfDecisions()];
+ for (int i = 0; i < _ATN.getNumberOfDecisions(); i++) {
+ _decisionToDFA[i] = new DFA(_ATN.getDecisionState(i), i);
+ }
+ }
+}
\ No newline at end of file
diff --git a/latte/src/main/java/refinements/RefinementsLanguage.g4 b/latte/src/main/java/refinements/RefinementsLanguage.g4
new file mode 100644
index 0000000..50d6fbb
--- /dev/null
+++ b/latte/src/main/java/refinements/RefinementsLanguage.g4
@@ -0,0 +1,58 @@
+grammar RefinementsLanguage;
+
+
+prog: pred | ;
+
+
+pred:
+ '(' pred ')' #predGroup
+ | '!' pred #predNegate
+ | pred LOGOP pred #predLogic
+ | pred '->' pred #predImplies
+ | exp #predExp
+ ;
+
+exp:
+ '(' exp ')' #expGroup
+ | exp BOOLOP exp #expBool
+ | operand #expOperand
+ ;
+
+operand:
+ leafs #opLiteral
+ | operand ARITHOP operand #opArith
+ | operand '-' operand #opSub
+ | '!' operand #opNot
+ | '(' operand ')' #opGroup
+ ;
+
+
+leafs:
+ '(' leafs ')' #litGroup
+ | literal #lit
+ | ID #var
+ | ID '.' ID #targetInvocation
+ ;
+
+
+literal:
+ BOOL #litBool
+ | INT #litInt
+ ;
+
+
+
+LOGOP : '&&'|'||';
+BOOLOP: '==' | '<=' | '<' | '>=' | '>';
+ARITHOP : '+'|'*'|'/';//|'-';
+
+// π | π₯ | π₯ .π | π + π | ! π
+// | π * π | π / π | π == π | π < π | π || π | π && π
+// | π₯ (π₯)
+
+BOOL : 'true' | 'false';
+ID_UPPER: ([A-Z][a-zA-Z0-9]*);
+ID : '#'*[a-zA-Z_][a-zA-Z0-9_#]*;
+INT : (([0-9]+) | ([0-9]+('_'[0-9]+)*));
+
+WS : (' '|'\t'|'\n'|'\r')+ -> channel(HIDDEN);
diff --git a/latte/src/main/java/refinements/RefinementsLanguage.interp b/latte/src/main/java/refinements/RefinementsLanguage.interp
new file mode 100644
index 0000000..d37f1d5
--- /dev/null
+++ b/latte/src/main/java/refinements/RefinementsLanguage.interp
@@ -0,0 +1,45 @@
+token literal names:
+null
+'('
+')'
+'!'
+'->'
+'-'
+'.'
+null
+null
+null
+null
+null
+null
+null
+null
+
+token symbolic names:
+null
+null
+null
+null
+null
+null
+null
+LOGOP
+BOOLOP
+ARITHOP
+BOOL
+ID_UPPER
+ID
+INT
+WS
+
+rule names:
+prog
+pred
+exp
+operand
+leafs
+literal
+
+
+atn:
+[4, 1, 14, 90, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 1, 0, 1, 0, 3, 0, 15, 8, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 3, 1, 25, 8, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 5, 1, 33, 8, 1, 10, 1, 12, 1, 36, 9, 1, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 3, 2, 44, 8, 2, 1, 2, 1, 2, 1, 2, 5, 2, 49, 8, 2, 10, 2, 12, 2, 52, 9, 2, 1, 3, 1, 3, 1, 3, 1, 3, 1, 3, 1, 3, 1, 3, 1, 3, 3, 3, 62, 8, 3, 1, 3, 1, 3, 1, 3, 1, 3, 1, 3, 1, 3, 5, 3, 70, 8, 3, 10, 3, 12, 3, 73, 9, 3, 1, 4, 1, 4, 1, 4, 1, 4, 1, 4, 1, 4, 1, 4, 1, 4, 1, 4, 3, 4, 84, 8, 4, 1, 5, 1, 5, 3, 5, 88, 8, 5, 1, 5, 0, 3, 2, 4, 6, 6, 0, 2, 4, 6, 8, 10, 0, 0, 98, 0, 14, 1, 0, 0, 0, 2, 24, 1, 0, 0, 0, 4, 43, 1, 0, 0, 0, 6, 61, 1, 0, 0, 0, 8, 83, 1, 0, 0, 0, 10, 87, 1, 0, 0, 0, 12, 15, 3, 2, 1, 0, 13, 15, 1, 0, 0, 0, 14, 12, 1, 0, 0, 0, 14, 13, 1, 0, 0, 0, 15, 1, 1, 0, 0, 0, 16, 17, 6, 1, -1, 0, 17, 18, 5, 1, 0, 0, 18, 19, 3, 2, 1, 0, 19, 20, 5, 2, 0, 0, 20, 25, 1, 0, 0, 0, 21, 22, 5, 3, 0, 0, 22, 25, 3, 2, 1, 4, 23, 25, 3, 4, 2, 0, 24, 16, 1, 0, 0, 0, 24, 21, 1, 0, 0, 0, 24, 23, 1, 0, 0, 0, 25, 34, 1, 0, 0, 0, 26, 27, 10, 3, 0, 0, 27, 28, 5, 7, 0, 0, 28, 33, 3, 2, 1, 4, 29, 30, 10, 2, 0, 0, 30, 31, 5, 4, 0, 0, 31, 33, 3, 2, 1, 3, 32, 26, 1, 0, 0, 0, 32, 29, 1, 0, 0, 0, 33, 36, 1, 0, 0, 0, 34, 32, 1, 0, 0, 0, 34, 35, 1, 0, 0, 0, 35, 3, 1, 0, 0, 0, 36, 34, 1, 0, 0, 0, 37, 38, 6, 2, -1, 0, 38, 39, 5, 1, 0, 0, 39, 40, 3, 4, 2, 0, 40, 41, 5, 2, 0, 0, 41, 44, 1, 0, 0, 0, 42, 44, 3, 6, 3, 0, 43, 37, 1, 0, 0, 0, 43, 42, 1, 0, 0, 0, 44, 50, 1, 0, 0, 0, 45, 46, 10, 2, 0, 0, 46, 47, 5, 8, 0, 0, 47, 49, 3, 4, 2, 3, 48, 45, 1, 0, 0, 0, 49, 52, 1, 0, 0, 0, 50, 48, 1, 0, 0, 0, 50, 51, 1, 0, 0, 0, 51, 5, 1, 0, 0, 0, 52, 50, 1, 0, 0, 0, 53, 54, 6, 3, -1, 0, 54, 62, 3, 8, 4, 0, 55, 56, 5, 3, 0, 0, 56, 62, 3, 6, 3, 2, 57, 58, 5, 1, 0, 0, 58, 59, 3, 6, 3, 0, 59, 60, 5, 2, 0, 0, 60, 62, 1, 0, 0, 0, 61, 53, 1, 0, 0, 0, 61, 55, 1, 0, 0, 0, 61, 57, 1, 0, 0, 0, 62, 71, 1, 0, 0, 0, 63, 64, 10, 4, 0, 0, 64, 65, 5, 9, 0, 0, 65, 70, 3, 6, 3, 5, 66, 67, 10, 3, 0, 0, 67, 68, 5, 5, 0, 0, 68, 70, 3, 6, 3, 4, 69, 63, 1, 0, 0, 0, 69, 66, 1, 0, 0, 0, 70, 73, 1, 0, 0, 0, 71, 69, 1, 0, 0, 0, 71, 72, 1, 0, 0, 0, 72, 7, 1, 0, 0, 0, 73, 71, 1, 0, 0, 0, 74, 75, 5, 1, 0, 0, 75, 76, 3, 8, 4, 0, 76, 77, 5, 2, 0, 0, 77, 84, 1, 0, 0, 0, 78, 84, 3, 10, 5, 0, 79, 84, 5, 12, 0, 0, 80, 81, 5, 12, 0, 0, 81, 82, 5, 6, 0, 0, 82, 84, 5, 12, 0, 0, 83, 74, 1, 0, 0, 0, 83, 78, 1, 0, 0, 0, 83, 79, 1, 0, 0, 0, 83, 80, 1, 0, 0, 0, 84, 9, 1, 0, 0, 0, 85, 88, 5, 10, 0, 0, 86, 88, 5, 13, 0, 0, 87, 85, 1, 0, 0, 0, 87, 86, 1, 0, 0, 0, 88, 11, 1, 0, 0, 0, 11, 14, 24, 32, 34, 43, 50, 61, 69, 71, 83, 87]
\ No newline at end of file
diff --git a/latte/src/main/java/refinements/RefinementsLanguage.tokens b/latte/src/main/java/refinements/RefinementsLanguage.tokens
new file mode 100644
index 0000000..fa92ca5
--- /dev/null
+++ b/latte/src/main/java/refinements/RefinementsLanguage.tokens
@@ -0,0 +1,20 @@
+T__0=1
+T__1=2
+T__2=3
+T__3=4
+T__4=5
+T__5=6
+LOGOP=7
+BOOLOP=8
+ARITHOP=9
+BOOL=10
+ID_UPPER=11
+ID=12
+INT=13
+WS=14
+'('=1
+')'=2
+'!'=3
+'->'=4
+'-'=5
+'.'=6
diff --git a/latte/src/main/java/refinements/RefinementsLanguageBaseListener.java b/latte/src/main/java/refinements/RefinementsLanguageBaseListener.java
new file mode 100644
index 0000000..cdd4627
--- /dev/null
+++ b/latte/src/main/java/refinements/RefinementsLanguageBaseListener.java
@@ -0,0 +1,280 @@
+// Generated from RefinementsLanguage.g4 by ANTLR 4.13.1
+package refinements;
+
+import org.antlr.v4.runtime.ParserRuleContext;
+import org.antlr.v4.runtime.tree.ErrorNode;
+import org.antlr.v4.runtime.tree.TerminalNode;
+
+/**
+ * This class provides an empty implementation of {@link RefinementsLanguageListener},
+ * which can be extended to create a listener which only needs to handle a subset
+ * of the available methods.
+ */
+@SuppressWarnings("CheckReturnValue")
+public class RefinementsLanguageBaseListener implements RefinementsLanguageListener {
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterProg(RefinementsLanguageParser.ProgContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitProg(RefinementsLanguageParser.ProgContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterPredGroup(RefinementsLanguageParser.PredGroupContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitPredGroup(RefinementsLanguageParser.PredGroupContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterPredNegate(RefinementsLanguageParser.PredNegateContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitPredNegate(RefinementsLanguageParser.PredNegateContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterPredExp(RefinementsLanguageParser.PredExpContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitPredExp(RefinementsLanguageParser.PredExpContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterPredImplies(RefinementsLanguageParser.PredImpliesContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitPredImplies(RefinementsLanguageParser.PredImpliesContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterPredLogic(RefinementsLanguageParser.PredLogicContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitPredLogic(RefinementsLanguageParser.PredLogicContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterExpBool(RefinementsLanguageParser.ExpBoolContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitExpBool(RefinementsLanguageParser.ExpBoolContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterExpOperand(RefinementsLanguageParser.ExpOperandContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitExpOperand(RefinementsLanguageParser.ExpOperandContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterExpGroup(RefinementsLanguageParser.ExpGroupContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitExpGroup(RefinementsLanguageParser.ExpGroupContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterOpArith(RefinementsLanguageParser.OpArithContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitOpArith(RefinementsLanguageParser.OpArithContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterOpNot(RefinementsLanguageParser.OpNotContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitOpNot(RefinementsLanguageParser.OpNotContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterOpLiteral(RefinementsLanguageParser.OpLiteralContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitOpLiteral(RefinementsLanguageParser.OpLiteralContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterOpGroup(RefinementsLanguageParser.OpGroupContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitOpGroup(RefinementsLanguageParser.OpGroupContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterOpSub(RefinementsLanguageParser.OpSubContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitOpSub(RefinementsLanguageParser.OpSubContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterLitGroup(RefinementsLanguageParser.LitGroupContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitLitGroup(RefinementsLanguageParser.LitGroupContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterLit(RefinementsLanguageParser.LitContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitLit(RefinementsLanguageParser.LitContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterVar(RefinementsLanguageParser.VarContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitVar(RefinementsLanguageParser.VarContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterTargetInvocation(RefinementsLanguageParser.TargetInvocationContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitTargetInvocation(RefinementsLanguageParser.TargetInvocationContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterLitBool(RefinementsLanguageParser.LitBoolContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitLitBool(RefinementsLanguageParser.LitBoolContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterLitInt(RefinementsLanguageParser.LitIntContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitLitInt(RefinementsLanguageParser.LitIntContext ctx) { }
+
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void enterEveryRule(ParserRuleContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void exitEveryRule(ParserRuleContext ctx) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void visitTerminal(TerminalNode node) { }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation does nothing.
+ */
+ @Override public void visitErrorNode(ErrorNode node) { }
+}
\ No newline at end of file
diff --git a/latte/src/main/java/refinements/RefinementsLanguageBaseVisitor.java b/latte/src/main/java/refinements/RefinementsLanguageBaseVisitor.java
new file mode 100644
index 0000000..11513fe
--- /dev/null
+++ b/latte/src/main/java/refinements/RefinementsLanguageBaseVisitor.java
@@ -0,0 +1,155 @@
+// Generated from RefinementsLanguage.g4 by ANTLR 4.13.1
+package refinements;
+import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
+
+/**
+ * This class provides an empty implementation of {@link RefinementsLanguageVisitor},
+ * which can be extended to create a visitor which only needs to handle a subset
+ * of the available methods.
+ *
+ * @param The return type of the visit operation. Use {@link Void} for
+ * operations with no return type.
+ */
+@SuppressWarnings("CheckReturnValue")
+public class RefinementsLanguageBaseVisitor extends AbstractParseTreeVisitor implements RefinementsLanguageVisitor {
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitProg(RefinementsLanguageParser.ProgContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitPredGroup(RefinementsLanguageParser.PredGroupContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitPredNegate(RefinementsLanguageParser.PredNegateContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitPredExp(RefinementsLanguageParser.PredExpContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitPredImplies(RefinementsLanguageParser.PredImpliesContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitPredLogic(RefinementsLanguageParser.PredLogicContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitExpBool(RefinementsLanguageParser.ExpBoolContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitExpOperand(RefinementsLanguageParser.ExpOperandContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitExpGroup(RefinementsLanguageParser.ExpGroupContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitOpArith(RefinementsLanguageParser.OpArithContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitOpNot(RefinementsLanguageParser.OpNotContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitOpLiteral(RefinementsLanguageParser.OpLiteralContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitOpGroup(RefinementsLanguageParser.OpGroupContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitOpSub(RefinementsLanguageParser.OpSubContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitLitGroup(RefinementsLanguageParser.LitGroupContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitLit(RefinementsLanguageParser.LitContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitVar(RefinementsLanguageParser.VarContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitTargetInvocation(RefinementsLanguageParser.TargetInvocationContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitLitBool(RefinementsLanguageParser.LitBoolContext ctx) { return visitChildren(ctx); }
+ /**
+ * {@inheritDoc}
+ *
+ * The default implementation returns the result of calling
+ * {@link #visitChildren} on {@code ctx}.
+ */
+ @Override public T visitLitInt(RefinementsLanguageParser.LitIntContext ctx) { return visitChildren(ctx); }
+}
\ No newline at end of file
diff --git a/latte/src/main/java/refinements/RefinementsLanguageLexer.interp b/latte/src/main/java/refinements/RefinementsLanguageLexer.interp
new file mode 100644
index 0000000..13eda4e
--- /dev/null
+++ b/latte/src/main/java/refinements/RefinementsLanguageLexer.interp
@@ -0,0 +1,59 @@
+token literal names:
+null
+'('
+')'
+'!'
+'->'
+'-'
+'.'
+null
+null
+null
+null
+null
+null
+null
+null
+
+token symbolic names:
+null
+null
+null
+null
+null
+null
+null
+LOGOP
+BOOLOP
+ARITHOP
+BOOL
+ID_UPPER
+ID
+INT
+WS
+
+rule names:
+T__0
+T__1
+T__2
+T__3
+T__4
+T__5
+LOGOP
+BOOLOP
+ARITHOP
+BOOL
+ID_UPPER
+ID
+INT
+WS
+
+channel names:
+DEFAULT_TOKEN_CHANNEL
+HIDDEN
+
+mode names:
+DEFAULT_MODE
+
+atn:
+[4, 0, 14, 121, 6, -1, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 2, 6, 7, 6, 2, 7, 7, 7, 2, 8, 7, 8, 2, 9, 7, 9, 2, 10, 7, 10, 2, 11, 7, 11, 2, 12, 7, 12, 2, 13, 7, 13, 1, 0, 1, 0, 1, 1, 1, 1, 1, 2, 1, 2, 1, 3, 1, 3, 1, 3, 1, 4, 1, 4, 1, 5, 1, 5, 1, 6, 1, 6, 1, 6, 1, 6, 3, 6, 47, 8, 6, 1, 7, 1, 7, 1, 7, 1, 7, 1, 7, 1, 7, 1, 7, 1, 7, 3, 7, 57, 8, 7, 1, 8, 1, 8, 1, 9, 1, 9, 1, 9, 1, 9, 1, 9, 1, 9, 1, 9, 1, 9, 1, 9, 3, 9, 70, 8, 9, 1, 10, 1, 10, 5, 10, 74, 8, 10, 10, 10, 12, 10, 77, 9, 10, 1, 11, 5, 11, 80, 8, 11, 10, 11, 12, 11, 83, 9, 11, 1, 11, 1, 11, 5, 11, 87, 8, 11, 10, 11, 12, 11, 90, 9, 11, 1, 12, 4, 12, 93, 8, 12, 11, 12, 12, 12, 94, 1, 12, 4, 12, 98, 8, 12, 11, 12, 12, 12, 99, 1, 12, 1, 12, 4, 12, 104, 8, 12, 11, 12, 12, 12, 105, 5, 12, 108, 8, 12, 10, 12, 12, 12, 111, 9, 12, 3, 12, 113, 8, 12, 1, 13, 4, 13, 116, 8, 13, 11, 13, 12, 13, 117, 1, 13, 1, 13, 0, 0, 14, 1, 1, 3, 2, 5, 3, 7, 4, 9, 5, 11, 6, 13, 7, 15, 8, 17, 9, 19, 10, 21, 11, 23, 12, 25, 13, 27, 14, 1, 0, 7, 2, 0, 42, 43, 47, 47, 1, 0, 65, 90, 3, 0, 48, 57, 65, 90, 97, 122, 3, 0, 65, 90, 95, 95, 97, 122, 5, 0, 35, 35, 48, 57, 65, 90, 95, 95, 97, 122, 1, 0, 48, 57, 3, 0, 9, 10, 13, 13, 32, 32, 135, 0, 1, 1, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 5, 1, 0, 0, 0, 0, 7, 1, 0, 0, 0, 0, 9, 1, 0, 0, 0, 0, 11, 1, 0, 0, 0, 0, 13, 1, 0, 0, 0, 0, 15, 1, 0, 0, 0, 0, 17, 1, 0, 0, 0, 0, 19, 1, 0, 0, 0, 0, 21, 1, 0, 0, 0, 0, 23, 1, 0, 0, 0, 0, 25, 1, 0, 0, 0, 0, 27, 1, 0, 0, 0, 1, 29, 1, 0, 0, 0, 3, 31, 1, 0, 0, 0, 5, 33, 1, 0, 0, 0, 7, 35, 1, 0, 0, 0, 9, 38, 1, 0, 0, 0, 11, 40, 1, 0, 0, 0, 13, 46, 1, 0, 0, 0, 15, 56, 1, 0, 0, 0, 17, 58, 1, 0, 0, 0, 19, 69, 1, 0, 0, 0, 21, 71, 1, 0, 0, 0, 23, 81, 1, 0, 0, 0, 25, 112, 1, 0, 0, 0, 27, 115, 1, 0, 0, 0, 29, 30, 5, 40, 0, 0, 30, 2, 1, 0, 0, 0, 31, 32, 5, 41, 0, 0, 32, 4, 1, 0, 0, 0, 33, 34, 5, 33, 0, 0, 34, 6, 1, 0, 0, 0, 35, 36, 5, 45, 0, 0, 36, 37, 5, 62, 0, 0, 37, 8, 1, 0, 0, 0, 38, 39, 5, 45, 0, 0, 39, 10, 1, 0, 0, 0, 40, 41, 5, 46, 0, 0, 41, 12, 1, 0, 0, 0, 42, 43, 5, 38, 0, 0, 43, 47, 5, 38, 0, 0, 44, 45, 5, 124, 0, 0, 45, 47, 5, 124, 0, 0, 46, 42, 1, 0, 0, 0, 46, 44, 1, 0, 0, 0, 47, 14, 1, 0, 0, 0, 48, 49, 5, 61, 0, 0, 49, 57, 5, 61, 0, 0, 50, 51, 5, 60, 0, 0, 51, 57, 5, 61, 0, 0, 52, 57, 5, 60, 0, 0, 53, 54, 5, 62, 0, 0, 54, 57, 5, 61, 0, 0, 55, 57, 5, 62, 0, 0, 56, 48, 1, 0, 0, 0, 56, 50, 1, 0, 0, 0, 56, 52, 1, 0, 0, 0, 56, 53, 1, 0, 0, 0, 56, 55, 1, 0, 0, 0, 57, 16, 1, 0, 0, 0, 58, 59, 7, 0, 0, 0, 59, 18, 1, 0, 0, 0, 60, 61, 5, 116, 0, 0, 61, 62, 5, 114, 0, 0, 62, 63, 5, 117, 0, 0, 63, 70, 5, 101, 0, 0, 64, 65, 5, 102, 0, 0, 65, 66, 5, 97, 0, 0, 66, 67, 5, 108, 0, 0, 67, 68, 5, 115, 0, 0, 68, 70, 5, 101, 0, 0, 69, 60, 1, 0, 0, 0, 69, 64, 1, 0, 0, 0, 70, 20, 1, 0, 0, 0, 71, 75, 7, 1, 0, 0, 72, 74, 7, 2, 0, 0, 73, 72, 1, 0, 0, 0, 74, 77, 1, 0, 0, 0, 75, 73, 1, 0, 0, 0, 75, 76, 1, 0, 0, 0, 76, 22, 1, 0, 0, 0, 77, 75, 1, 0, 0, 0, 78, 80, 5, 35, 0, 0, 79, 78, 1, 0, 0, 0, 80, 83, 1, 0, 0, 0, 81, 79, 1, 0, 0, 0, 81, 82, 1, 0, 0, 0, 82, 84, 1, 0, 0, 0, 83, 81, 1, 0, 0, 0, 84, 88, 7, 3, 0, 0, 85, 87, 7, 4, 0, 0, 86, 85, 1, 0, 0, 0, 87, 90, 1, 0, 0, 0, 88, 86, 1, 0, 0, 0, 88, 89, 1, 0, 0, 0, 89, 24, 1, 0, 0, 0, 90, 88, 1, 0, 0, 0, 91, 93, 7, 5, 0, 0, 92, 91, 1, 0, 0, 0, 93, 94, 1, 0, 0, 0, 94, 92, 1, 0, 0, 0, 94, 95, 1, 0, 0, 0, 95, 113, 1, 0, 0, 0, 96, 98, 7, 5, 0, 0, 97, 96, 1, 0, 0, 0, 98, 99, 1, 0, 0, 0, 99, 97, 1, 0, 0, 0, 99, 100, 1, 0, 0, 0, 100, 109, 1, 0, 0, 0, 101, 103, 5, 95, 0, 0, 102, 104, 7, 5, 0, 0, 103, 102, 1, 0, 0, 0, 104, 105, 1, 0, 0, 0, 105, 103, 1, 0, 0, 0, 105, 106, 1, 0, 0, 0, 106, 108, 1, 0, 0, 0, 107, 101, 1, 0, 0, 0, 108, 111, 1, 0, 0, 0, 109, 107, 1, 0, 0, 0, 109, 110, 1, 0, 0, 0, 110, 113, 1, 0, 0, 0, 111, 109, 1, 0, 0, 0, 112, 92, 1, 0, 0, 0, 112, 97, 1, 0, 0, 0, 113, 26, 1, 0, 0, 0, 114, 116, 7, 6, 0, 0, 115, 114, 1, 0, 0, 0, 116, 117, 1, 0, 0, 0, 117, 115, 1, 0, 0, 0, 117, 118, 1, 0, 0, 0, 118, 119, 1, 0, 0, 0, 119, 120, 6, 13, 0, 0, 120, 28, 1, 0, 0, 0, 13, 0, 46, 56, 69, 75, 81, 88, 94, 99, 105, 109, 112, 117, 1, 0, 1, 0]
\ No newline at end of file
diff --git a/latte/src/main/java/refinements/RefinementsLanguageLexer.java b/latte/src/main/java/refinements/RefinementsLanguageLexer.java
new file mode 100644
index 0000000..fb8f21e
--- /dev/null
+++ b/latte/src/main/java/refinements/RefinementsLanguageLexer.java
@@ -0,0 +1,189 @@
+// Generated from RefinementsLanguage.g4 by ANTLR 4.13.1
+package refinements;
+import org.antlr.v4.runtime.Lexer;
+import org.antlr.v4.runtime.CharStream;
+import org.antlr.v4.runtime.Token;
+import org.antlr.v4.runtime.TokenStream;
+import org.antlr.v4.runtime.*;
+import org.antlr.v4.runtime.atn.*;
+import org.antlr.v4.runtime.dfa.DFA;
+import org.antlr.v4.runtime.misc.*;
+
+@SuppressWarnings({"all", "warnings", "unchecked", "unused", "cast", "CheckReturnValue", "this-escape"})
+public class RefinementsLanguageLexer extends Lexer {
+ static { RuntimeMetaData.checkVersion("4.13.1", RuntimeMetaData.VERSION); }
+
+ protected static final DFA[] _decisionToDFA;
+ protected static final PredictionContextCache _sharedContextCache =
+ new PredictionContextCache();
+ public static final int
+ T__0=1, T__1=2, T__2=3, T__3=4, T__4=5, T__5=6, LOGOP=7, BOOLOP=8, ARITHOP=9,
+ BOOL=10, ID_UPPER=11, ID=12, INT=13, WS=14;
+ public static String[] channelNames = {
+ "DEFAULT_TOKEN_CHANNEL", "HIDDEN"
+ };
+
+ public static String[] modeNames = {
+ "DEFAULT_MODE"
+ };
+
+ private static String[] makeRuleNames() {
+ return new String[] {
+ "T__0", "T__1", "T__2", "T__3", "T__4", "T__5", "LOGOP", "BOOLOP", "ARITHOP",
+ "BOOL", "ID_UPPER", "ID", "INT", "WS"
+ };
+ }
+ public static final String[] ruleNames = makeRuleNames();
+
+ private static String[] makeLiteralNames() {
+ return new String[] {
+ null, "'('", "')'", "'!'", "'->'", "'-'", "'.'"
+ };
+ }
+ private static final String[] _LITERAL_NAMES = makeLiteralNames();
+ private static String[] makeSymbolicNames() {
+ return new String[] {
+ null, null, null, null, null, null, null, "LOGOP", "BOOLOP", "ARITHOP",
+ "BOOL", "ID_UPPER", "ID", "INT", "WS"
+ };
+ }
+ private static final String[] _SYMBOLIC_NAMES = makeSymbolicNames();
+ public static final Vocabulary VOCABULARY = new VocabularyImpl(_LITERAL_NAMES, _SYMBOLIC_NAMES);
+
+ /**
+ * @deprecated Use {@link #VOCABULARY} instead.
+ */
+ @Deprecated
+ public static final String[] tokenNames;
+ static {
+ tokenNames = new String[_SYMBOLIC_NAMES.length];
+ for (int i = 0; i < tokenNames.length; i++) {
+ tokenNames[i] = VOCABULARY.getLiteralName(i);
+ if (tokenNames[i] == null) {
+ tokenNames[i] = VOCABULARY.getSymbolicName(i);
+ }
+
+ if (tokenNames[i] == null) {
+ tokenNames[i] = "";
+ }
+ }
+ }
+
+ @Override
+ @Deprecated
+ public String[] getTokenNames() {
+ return tokenNames;
+ }
+
+ @Override
+
+ public Vocabulary getVocabulary() {
+ return VOCABULARY;
+ }
+
+
+ public RefinementsLanguageLexer(CharStream input) {
+ super(input);
+ _interp = new LexerATNSimulator(this,_ATN,_decisionToDFA,_sharedContextCache);
+ }
+
+ @Override
+ public String getGrammarFileName() { return "RefinementsLanguage.g4"; }
+
+ @Override
+ public String[] getRuleNames() { return ruleNames; }
+
+ @Override
+ public String getSerializedATN() { return _serializedATN; }
+
+ @Override
+ public String[] getChannelNames() { return channelNames; }
+
+ @Override
+ public String[] getModeNames() { return modeNames; }
+
+ @Override
+ public ATN getATN() { return _ATN; }
+
+ public static final String _serializedATN =
+ "\u0004\u0000\u000ey\u0006\uffff\uffff\u0002\u0000\u0007\u0000\u0002\u0001"+
+ "\u0007\u0001\u0002\u0002\u0007\u0002\u0002\u0003\u0007\u0003\u0002\u0004"+
+ "\u0007\u0004\u0002\u0005\u0007\u0005\u0002\u0006\u0007\u0006\u0002\u0007"+
+ "\u0007\u0007\u0002\b\u0007\b\u0002\t\u0007\t\u0002\n\u0007\n\u0002\u000b"+
+ "\u0007\u000b\u0002\f\u0007\f\u0002\r\u0007\r\u0001\u0000\u0001\u0000\u0001"+
+ "\u0001\u0001\u0001\u0001\u0002\u0001\u0002\u0001\u0003\u0001\u0003\u0001"+
+ "\u0003\u0001\u0004\u0001\u0004\u0001\u0005\u0001\u0005\u0001\u0006\u0001"+
+ "\u0006\u0001\u0006\u0001\u0006\u0003\u0006/\b\u0006\u0001\u0007\u0001"+
+ "\u0007\u0001\u0007\u0001\u0007\u0001\u0007\u0001\u0007\u0001\u0007\u0001"+
+ "\u0007\u0003\u00079\b\u0007\u0001\b\u0001\b\u0001\t\u0001\t\u0001\t\u0001"+
+ "\t\u0001\t\u0001\t\u0001\t\u0001\t\u0001\t\u0003\tF\b\t\u0001\n\u0001"+
+ "\n\u0005\nJ\b\n\n\n\f\nM\t\n\u0001\u000b\u0005\u000bP\b\u000b\n\u000b"+
+ "\f\u000bS\t\u000b\u0001\u000b\u0001\u000b\u0005\u000bW\b\u000b\n\u000b"+
+ "\f\u000bZ\t\u000b\u0001\f\u0004\f]\b\f\u000b\f\f\f^\u0001\f\u0004\fb\b"+
+ "\f\u000b\f\f\fc\u0001\f\u0001\f\u0004\fh\b\f\u000b\f\f\fi\u0005\fl\b\f"+
+ "\n\f\f\fo\t\f\u0003\fq\b\f\u0001\r\u0004\rt\b\r\u000b\r\f\ru\u0001\r\u0001"+
+ "\r\u0000\u0000\u000e\u0001\u0001\u0003\u0002\u0005\u0003\u0007\u0004\t"+
+ "\u0005\u000b\u0006\r\u0007\u000f\b\u0011\t\u0013\n\u0015\u000b\u0017\f"+
+ "\u0019\r\u001b\u000e\u0001\u0000\u0007\u0002\u0000*+//\u0001\u0000AZ\u0003"+
+ "\u000009AZaz\u0003\u0000AZ__az\u0005\u0000##09AZ__az\u0001\u000009\u0003"+
+ "\u0000\t\n\r\r \u0087\u0000\u0001\u0001\u0000\u0000\u0000\u0000\u0003"+
+ "\u0001\u0000\u0000\u0000\u0000\u0005\u0001\u0000\u0000\u0000\u0000\u0007"+
+ "\u0001\u0000\u0000\u0000\u0000\t\u0001\u0000\u0000\u0000\u0000\u000b\u0001"+
+ "\u0000\u0000\u0000\u0000\r\u0001\u0000\u0000\u0000\u0000\u000f\u0001\u0000"+
+ "\u0000\u0000\u0000\u0011\u0001\u0000\u0000\u0000\u0000\u0013\u0001\u0000"+
+ "\u0000\u0000\u0000\u0015\u0001\u0000\u0000\u0000\u0000\u0017\u0001\u0000"+
+ "\u0000\u0000\u0000\u0019\u0001\u0000\u0000\u0000\u0000\u001b\u0001\u0000"+
+ "\u0000\u0000\u0001\u001d\u0001\u0000\u0000\u0000\u0003\u001f\u0001\u0000"+
+ "\u0000\u0000\u0005!\u0001\u0000\u0000\u0000\u0007#\u0001\u0000\u0000\u0000"+
+ "\t&\u0001\u0000\u0000\u0000\u000b(\u0001\u0000\u0000\u0000\r.\u0001\u0000"+
+ "\u0000\u0000\u000f8\u0001\u0000\u0000\u0000\u0011:\u0001\u0000\u0000\u0000"+
+ "\u0013E\u0001\u0000\u0000\u0000\u0015G\u0001\u0000\u0000\u0000\u0017Q"+
+ "\u0001\u0000\u0000\u0000\u0019p\u0001\u0000\u0000\u0000\u001bs\u0001\u0000"+
+ "\u0000\u0000\u001d\u001e\u0005(\u0000\u0000\u001e\u0002\u0001\u0000\u0000"+
+ "\u0000\u001f \u0005)\u0000\u0000 \u0004\u0001\u0000\u0000\u0000!\"\u0005"+
+ "!\u0000\u0000\"\u0006\u0001\u0000\u0000\u0000#$\u0005-\u0000\u0000$%\u0005"+
+ ">\u0000\u0000%\b\u0001\u0000\u0000\u0000&\'\u0005-\u0000\u0000\'\n\u0001"+
+ "\u0000\u0000\u0000()\u0005.\u0000\u0000)\f\u0001\u0000\u0000\u0000*+\u0005"+
+ "&\u0000\u0000+/\u0005&\u0000\u0000,-\u0005|\u0000\u0000-/\u0005|\u0000"+
+ "\u0000.*\u0001\u0000\u0000\u0000.,\u0001\u0000\u0000\u0000/\u000e\u0001"+
+ "\u0000\u0000\u000001\u0005=\u0000\u000019\u0005=\u0000\u000023\u0005<"+
+ "\u0000\u000039\u0005=\u0000\u000049\u0005<\u0000\u000056\u0005>\u0000"+
+ "\u000069\u0005=\u0000\u000079\u0005>\u0000\u000080\u0001\u0000\u0000\u0000"+
+ "82\u0001\u0000\u0000\u000084\u0001\u0000\u0000\u000085\u0001\u0000\u0000"+
+ "\u000087\u0001\u0000\u0000\u00009\u0010\u0001\u0000\u0000\u0000:;\u0007"+
+ "\u0000\u0000\u0000;\u0012\u0001\u0000\u0000\u0000<=\u0005t\u0000\u0000"+
+ "=>\u0005r\u0000\u0000>?\u0005u\u0000\u0000?F\u0005e\u0000\u0000@A\u0005"+
+ "f\u0000\u0000AB\u0005a\u0000\u0000BC\u0005l\u0000\u0000CD\u0005s\u0000"+
+ "\u0000DF\u0005e\u0000\u0000E<\u0001\u0000\u0000\u0000E@\u0001\u0000\u0000"+
+ "\u0000F\u0014\u0001\u0000\u0000\u0000GK\u0007\u0001\u0000\u0000HJ\u0007"+
+ "\u0002\u0000\u0000IH\u0001\u0000\u0000\u0000JM\u0001\u0000\u0000\u0000"+
+ "KI\u0001\u0000\u0000\u0000KL\u0001\u0000\u0000\u0000L\u0016\u0001\u0000"+
+ "\u0000\u0000MK\u0001\u0000\u0000\u0000NP\u0005#\u0000\u0000ON\u0001\u0000"+
+ "\u0000\u0000PS\u0001\u0000\u0000\u0000QO\u0001\u0000\u0000\u0000QR\u0001"+
+ "\u0000\u0000\u0000RT\u0001\u0000\u0000\u0000SQ\u0001\u0000\u0000\u0000"+
+ "TX\u0007\u0003\u0000\u0000UW\u0007\u0004\u0000\u0000VU\u0001\u0000\u0000"+
+ "\u0000WZ\u0001\u0000\u0000\u0000XV\u0001\u0000\u0000\u0000XY\u0001\u0000"+
+ "\u0000\u0000Y\u0018\u0001\u0000\u0000\u0000ZX\u0001\u0000\u0000\u0000"+
+ "[]\u0007\u0005\u0000\u0000\\[\u0001\u0000\u0000\u0000]^\u0001\u0000\u0000"+
+ "\u0000^\\\u0001\u0000\u0000\u0000^_\u0001\u0000\u0000\u0000_q\u0001\u0000"+
+ "\u0000\u0000`b\u0007\u0005\u0000\u0000a`\u0001\u0000\u0000\u0000bc\u0001"+
+ "\u0000\u0000\u0000ca\u0001\u0000\u0000\u0000cd\u0001\u0000\u0000\u0000"+
+ "dm\u0001\u0000\u0000\u0000eg\u0005_\u0000\u0000fh\u0007\u0005\u0000\u0000"+
+ "gf\u0001\u0000\u0000\u0000hi\u0001\u0000\u0000\u0000ig\u0001\u0000\u0000"+
+ "\u0000ij\u0001\u0000\u0000\u0000jl\u0001\u0000\u0000\u0000ke\u0001\u0000"+
+ "\u0000\u0000lo\u0001\u0000\u0000\u0000mk\u0001\u0000\u0000\u0000mn\u0001"+
+ "\u0000\u0000\u0000nq\u0001\u0000\u0000\u0000om\u0001\u0000\u0000\u0000"+
+ "p\\\u0001\u0000\u0000\u0000pa\u0001\u0000\u0000\u0000q\u001a\u0001\u0000"+
+ "\u0000\u0000rt\u0007\u0006\u0000\u0000sr\u0001\u0000\u0000\u0000tu\u0001"+
+ "\u0000\u0000\u0000us\u0001\u0000\u0000\u0000uv\u0001\u0000\u0000\u0000"+
+ "vw\u0001\u0000\u0000\u0000wx\u0006\r\u0000\u0000x\u001c\u0001\u0000\u0000"+
+ "\u0000\r\u0000.8EKQX^cimpu\u0001\u0000\u0001\u0000";
+ public static final ATN _ATN =
+ new ATNDeserializer().deserialize(_serializedATN.toCharArray());
+ static {
+ _decisionToDFA = new DFA[_ATN.getNumberOfDecisions()];
+ for (int i = 0; i < _ATN.getNumberOfDecisions(); i++) {
+ _decisionToDFA[i] = new DFA(_ATN.getDecisionState(i), i);
+ }
+ }
+}
\ No newline at end of file
diff --git a/latte/src/main/java/refinements/RefinementsLanguageLexer.tokens b/latte/src/main/java/refinements/RefinementsLanguageLexer.tokens
new file mode 100644
index 0000000..fa92ca5
--- /dev/null
+++ b/latte/src/main/java/refinements/RefinementsLanguageLexer.tokens
@@ -0,0 +1,20 @@
+T__0=1
+T__1=2
+T__2=3
+T__3=4
+T__4=5
+T__5=6
+LOGOP=7
+BOOLOP=8
+ARITHOP=9
+BOOL=10
+ID_UPPER=11
+ID=12
+INT=13
+WS=14
+'('=1
+')'=2
+'!'=3
+'->'=4
+'-'=5
+'.'=6
diff --git a/latte/src/main/java/refinements/RefinementsLanguageListener.java b/latte/src/main/java/refinements/RefinementsLanguageListener.java
new file mode 100644
index 0000000..4df1111
--- /dev/null
+++ b/latte/src/main/java/refinements/RefinementsLanguageListener.java
@@ -0,0 +1,248 @@
+// Generated from RefinementsLanguage.g4 by ANTLR 4.13.1
+package refinements;
+import org.antlr.v4.runtime.tree.ParseTreeListener;
+
+/**
+ * This interface defines a complete listener for a parse tree produced by
+ * {@link RefinementsLanguageParser}.
+ */
+public interface RefinementsLanguageListener extends ParseTreeListener {
+ /**
+ * Enter a parse tree produced by {@link RefinementsLanguageParser#prog}.
+ * @param ctx the parse tree
+ */
+ void enterProg(RefinementsLanguageParser.ProgContext ctx);
+ /**
+ * Exit a parse tree produced by {@link RefinementsLanguageParser#prog}.
+ * @param ctx the parse tree
+ */
+ void exitProg(RefinementsLanguageParser.ProgContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code predGroup}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ */
+ void enterPredGroup(RefinementsLanguageParser.PredGroupContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code predGroup}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ */
+ void exitPredGroup(RefinementsLanguageParser.PredGroupContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code predNegate}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ */
+ void enterPredNegate(RefinementsLanguageParser.PredNegateContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code predNegate}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ */
+ void exitPredNegate(RefinementsLanguageParser.PredNegateContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code predExp}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ */
+ void enterPredExp(RefinementsLanguageParser.PredExpContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code predExp}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ */
+ void exitPredExp(RefinementsLanguageParser.PredExpContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code predImplies}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ */
+ void enterPredImplies(RefinementsLanguageParser.PredImpliesContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code predImplies}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ */
+ void exitPredImplies(RefinementsLanguageParser.PredImpliesContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code predLogic}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ */
+ void enterPredLogic(RefinementsLanguageParser.PredLogicContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code predLogic}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ */
+ void exitPredLogic(RefinementsLanguageParser.PredLogicContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code expBool}
+ * labeled alternative in {@link RefinementsLanguageParser#exp}.
+ * @param ctx the parse tree
+ */
+ void enterExpBool(RefinementsLanguageParser.ExpBoolContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code expBool}
+ * labeled alternative in {@link RefinementsLanguageParser#exp}.
+ * @param ctx the parse tree
+ */
+ void exitExpBool(RefinementsLanguageParser.ExpBoolContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code expOperand}
+ * labeled alternative in {@link RefinementsLanguageParser#exp}.
+ * @param ctx the parse tree
+ */
+ void enterExpOperand(RefinementsLanguageParser.ExpOperandContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code expOperand}
+ * labeled alternative in {@link RefinementsLanguageParser#exp}.
+ * @param ctx the parse tree
+ */
+ void exitExpOperand(RefinementsLanguageParser.ExpOperandContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code expGroup}
+ * labeled alternative in {@link RefinementsLanguageParser#exp}.
+ * @param ctx the parse tree
+ */
+ void enterExpGroup(RefinementsLanguageParser.ExpGroupContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code expGroup}
+ * labeled alternative in {@link RefinementsLanguageParser#exp}.
+ * @param ctx the parse tree
+ */
+ void exitExpGroup(RefinementsLanguageParser.ExpGroupContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code opArith}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ */
+ void enterOpArith(RefinementsLanguageParser.OpArithContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code opArith}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ */
+ void exitOpArith(RefinementsLanguageParser.OpArithContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code opNot}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ */
+ void enterOpNot(RefinementsLanguageParser.OpNotContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code opNot}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ */
+ void exitOpNot(RefinementsLanguageParser.OpNotContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code opLiteral}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ */
+ void enterOpLiteral(RefinementsLanguageParser.OpLiteralContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code opLiteral}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ */
+ void exitOpLiteral(RefinementsLanguageParser.OpLiteralContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code opGroup}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ */
+ void enterOpGroup(RefinementsLanguageParser.OpGroupContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code opGroup}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ */
+ void exitOpGroup(RefinementsLanguageParser.OpGroupContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code opSub}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ */
+ void enterOpSub(RefinementsLanguageParser.OpSubContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code opSub}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ */
+ void exitOpSub(RefinementsLanguageParser.OpSubContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code litGroup}
+ * labeled alternative in {@link RefinementsLanguageParser#leafs}.
+ * @param ctx the parse tree
+ */
+ void enterLitGroup(RefinementsLanguageParser.LitGroupContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code litGroup}
+ * labeled alternative in {@link RefinementsLanguageParser#leafs}.
+ * @param ctx the parse tree
+ */
+ void exitLitGroup(RefinementsLanguageParser.LitGroupContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code lit}
+ * labeled alternative in {@link RefinementsLanguageParser#leafs}.
+ * @param ctx the parse tree
+ */
+ void enterLit(RefinementsLanguageParser.LitContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code lit}
+ * labeled alternative in {@link RefinementsLanguageParser#leafs}.
+ * @param ctx the parse tree
+ */
+ void exitLit(RefinementsLanguageParser.LitContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code var}
+ * labeled alternative in {@link RefinementsLanguageParser#leafs}.
+ * @param ctx the parse tree
+ */
+ void enterVar(RefinementsLanguageParser.VarContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code var}
+ * labeled alternative in {@link RefinementsLanguageParser#leafs}.
+ * @param ctx the parse tree
+ */
+ void exitVar(RefinementsLanguageParser.VarContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code targetInvocation}
+ * labeled alternative in {@link RefinementsLanguageParser#leafs}.
+ * @param ctx the parse tree
+ */
+ void enterTargetInvocation(RefinementsLanguageParser.TargetInvocationContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code targetInvocation}
+ * labeled alternative in {@link RefinementsLanguageParser#leafs}.
+ * @param ctx the parse tree
+ */
+ void exitTargetInvocation(RefinementsLanguageParser.TargetInvocationContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code litBool}
+ * labeled alternative in {@link RefinementsLanguageParser#literal}.
+ * @param ctx the parse tree
+ */
+ void enterLitBool(RefinementsLanguageParser.LitBoolContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code litBool}
+ * labeled alternative in {@link RefinementsLanguageParser#literal}.
+ * @param ctx the parse tree
+ */
+ void exitLitBool(RefinementsLanguageParser.LitBoolContext ctx);
+ /**
+ * Enter a parse tree produced by the {@code litInt}
+ * labeled alternative in {@link RefinementsLanguageParser#literal}.
+ * @param ctx the parse tree
+ */
+ void enterLitInt(RefinementsLanguageParser.LitIntContext ctx);
+ /**
+ * Exit a parse tree produced by the {@code litInt}
+ * labeled alternative in {@link RefinementsLanguageParser#literal}.
+ * @param ctx the parse tree
+ */
+ void exitLitInt(RefinementsLanguageParser.LitIntContext ctx);
+}
\ No newline at end of file
diff --git a/latte/src/main/java/refinements/RefinementsLanguageParser.java b/latte/src/main/java/refinements/RefinementsLanguageParser.java
new file mode 100644
index 0000000..9d0eb20
--- /dev/null
+++ b/latte/src/main/java/refinements/RefinementsLanguageParser.java
@@ -0,0 +1,1112 @@
+// Generated from RefinementsLanguage.g4 by ANTLR 4.13.1
+package refinements;
+import org.antlr.v4.runtime.atn.*;
+import org.antlr.v4.runtime.dfa.DFA;
+import org.antlr.v4.runtime.*;
+import org.antlr.v4.runtime.misc.*;
+import org.antlr.v4.runtime.tree.*;
+import java.util.List;
+import java.util.Iterator;
+import java.util.ArrayList;
+
+@SuppressWarnings({"all", "warnings", "unchecked", "unused", "cast", "CheckReturnValue"})
+public class RefinementsLanguageParser extends Parser {
+ static { RuntimeMetaData.checkVersion("4.13.1", RuntimeMetaData.VERSION); }
+
+ protected static final DFA[] _decisionToDFA;
+ protected static final PredictionContextCache _sharedContextCache =
+ new PredictionContextCache();
+ public static final int
+ T__0=1, T__1=2, T__2=3, T__3=4, T__4=5, T__5=6, LOGOP=7, BOOLOP=8, ARITHOP=9,
+ BOOL=10, ID_UPPER=11, ID=12, INT=13, WS=14;
+ public static final int
+ RULE_prog = 0, RULE_pred = 1, RULE_exp = 2, RULE_operand = 3, RULE_leafs = 4,
+ RULE_literal = 5;
+ private static String[] makeRuleNames() {
+ return new String[] {
+ "prog", "pred", "exp", "operand", "leafs", "literal"
+ };
+ }
+ public static final String[] ruleNames = makeRuleNames();
+
+ private static String[] makeLiteralNames() {
+ return new String[] {
+ null, "'('", "')'", "'!'", "'->'", "'-'", "'.'"
+ };
+ }
+ private static final String[] _LITERAL_NAMES = makeLiteralNames();
+ private static String[] makeSymbolicNames() {
+ return new String[] {
+ null, null, null, null, null, null, null, "LOGOP", "BOOLOP", "ARITHOP",
+ "BOOL", "ID_UPPER", "ID", "INT", "WS"
+ };
+ }
+ private static final String[] _SYMBOLIC_NAMES = makeSymbolicNames();
+ public static final Vocabulary VOCABULARY = new VocabularyImpl(_LITERAL_NAMES, _SYMBOLIC_NAMES);
+
+ /**
+ * @deprecated Use {@link #VOCABULARY} instead.
+ */
+ @Deprecated
+ public static final String[] tokenNames;
+ static {
+ tokenNames = new String[_SYMBOLIC_NAMES.length];
+ for (int i = 0; i < tokenNames.length; i++) {
+ tokenNames[i] = VOCABULARY.getLiteralName(i);
+ if (tokenNames[i] == null) {
+ tokenNames[i] = VOCABULARY.getSymbolicName(i);
+ }
+
+ if (tokenNames[i] == null) {
+ tokenNames[i] = "";
+ }
+ }
+ }
+
+ @Override
+ @Deprecated
+ public String[] getTokenNames() {
+ return tokenNames;
+ }
+
+ @Override
+
+ public Vocabulary getVocabulary() {
+ return VOCABULARY;
+ }
+
+ @Override
+ public String getGrammarFileName() { return "RefinementsLanguage.g4"; }
+
+ @Override
+ public String[] getRuleNames() { return ruleNames; }
+
+ @Override
+ public String getSerializedATN() { return _serializedATN; }
+
+ @Override
+ public ATN getATN() { return _ATN; }
+
+ public RefinementsLanguageParser(TokenStream input) {
+ super(input);
+ _interp = new ParserATNSimulator(this,_ATN,_decisionToDFA,_sharedContextCache);
+ }
+
+ @SuppressWarnings("CheckReturnValue")
+ public static class ProgContext extends ParserRuleContext {
+ public PredContext pred() {
+ return getRuleContext(PredContext.class,0);
+ }
+ public ProgContext(ParserRuleContext parent, int invokingState) {
+ super(parent, invokingState);
+ }
+ @Override public int getRuleIndex() { return RULE_prog; }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterProg(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitProg(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitProg(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+
+ public final ProgContext prog() throws RecognitionException {
+ ProgContext _localctx = new ProgContext(_ctx, getState());
+ enterRule(_localctx, 0, RULE_prog);
+ try {
+ setState(14);
+ _errHandler.sync(this);
+ switch (_input.LA(1)) {
+ case T__0:
+ case T__2:
+ case BOOL:
+ case ID:
+ case INT:
+ enterOuterAlt(_localctx, 1);
+ {
+ setState(12);
+ pred(0);
+ }
+ break;
+ case EOF:
+ enterOuterAlt(_localctx, 2);
+ {
+ }
+ break;
+ default:
+ throw new NoViableAltException(this);
+ }
+ }
+ catch (RecognitionException re) {
+ _localctx.exception = re;
+ _errHandler.reportError(this, re);
+ _errHandler.recover(this, re);
+ }
+ finally {
+ exitRule();
+ }
+ return _localctx;
+ }
+
+ @SuppressWarnings("CheckReturnValue")
+ public static class PredContext extends ParserRuleContext {
+ public PredContext(ParserRuleContext parent, int invokingState) {
+ super(parent, invokingState);
+ }
+ @Override public int getRuleIndex() { return RULE_pred; }
+
+ public PredContext() { }
+ public void copyFrom(PredContext ctx) {
+ super.copyFrom(ctx);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class PredGroupContext extends PredContext {
+ public PredContext pred() {
+ return getRuleContext(PredContext.class,0);
+ }
+ public PredGroupContext(PredContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterPredGroup(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitPredGroup(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitPredGroup(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class PredNegateContext extends PredContext {
+ public PredContext pred() {
+ return getRuleContext(PredContext.class,0);
+ }
+ public PredNegateContext(PredContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterPredNegate(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitPredNegate(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitPredNegate(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class PredExpContext extends PredContext {
+ public ExpContext exp() {
+ return getRuleContext(ExpContext.class,0);
+ }
+ public PredExpContext(PredContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterPredExp(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitPredExp(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitPredExp(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class PredImpliesContext extends PredContext {
+ public List pred() {
+ return getRuleContexts(PredContext.class);
+ }
+ public PredContext pred(int i) {
+ return getRuleContext(PredContext.class,i);
+ }
+ public PredImpliesContext(PredContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterPredImplies(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitPredImplies(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitPredImplies(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class PredLogicContext extends PredContext {
+ public List pred() {
+ return getRuleContexts(PredContext.class);
+ }
+ public PredContext pred(int i) {
+ return getRuleContext(PredContext.class,i);
+ }
+ public TerminalNode LOGOP() { return getToken(RefinementsLanguageParser.LOGOP, 0); }
+ public PredLogicContext(PredContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterPredLogic(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitPredLogic(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitPredLogic(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+
+ public final PredContext pred() throws RecognitionException {
+ return pred(0);
+ }
+
+ private PredContext pred(int _p) throws RecognitionException {
+ ParserRuleContext _parentctx = _ctx;
+ int _parentState = getState();
+ PredContext _localctx = new PredContext(_ctx, _parentState);
+ PredContext _prevctx = _localctx;
+ int _startState = 2;
+ enterRecursionRule(_localctx, 2, RULE_pred, _p);
+ try {
+ int _alt;
+ enterOuterAlt(_localctx, 1);
+ {
+ setState(24);
+ _errHandler.sync(this);
+ switch ( getInterpreter().adaptivePredict(_input,1,_ctx) ) {
+ case 1:
+ {
+ _localctx = new PredGroupContext(_localctx);
+ _ctx = _localctx;
+ _prevctx = _localctx;
+
+ setState(17);
+ match(T__0);
+ setState(18);
+ pred(0);
+ setState(19);
+ match(T__1);
+ }
+ break;
+ case 2:
+ {
+ _localctx = new PredNegateContext(_localctx);
+ _ctx = _localctx;
+ _prevctx = _localctx;
+ setState(21);
+ match(T__2);
+ setState(22);
+ pred(4);
+ }
+ break;
+ case 3:
+ {
+ _localctx = new PredExpContext(_localctx);
+ _ctx = _localctx;
+ _prevctx = _localctx;
+ setState(23);
+ exp(0);
+ }
+ break;
+ }
+ _ctx.stop = _input.LT(-1);
+ setState(34);
+ _errHandler.sync(this);
+ _alt = getInterpreter().adaptivePredict(_input,3,_ctx);
+ while ( _alt!=2 && _alt!=org.antlr.v4.runtime.atn.ATN.INVALID_ALT_NUMBER ) {
+ if ( _alt==1 ) {
+ if ( _parseListeners!=null ) triggerExitRuleEvent();
+ _prevctx = _localctx;
+ {
+ setState(32);
+ _errHandler.sync(this);
+ switch ( getInterpreter().adaptivePredict(_input,2,_ctx) ) {
+ case 1:
+ {
+ _localctx = new PredLogicContext(new PredContext(_parentctx, _parentState));
+ pushNewRecursionContext(_localctx, _startState, RULE_pred);
+ setState(26);
+ if (!(precpred(_ctx, 3))) throw new FailedPredicateException(this, "precpred(_ctx, 3)");
+ setState(27);
+ match(LOGOP);
+ setState(28);
+ pred(4);
+ }
+ break;
+ case 2:
+ {
+ _localctx = new PredImpliesContext(new PredContext(_parentctx, _parentState));
+ pushNewRecursionContext(_localctx, _startState, RULE_pred);
+ setState(29);
+ if (!(precpred(_ctx, 2))) throw new FailedPredicateException(this, "precpred(_ctx, 2)");
+ setState(30);
+ match(T__3);
+ setState(31);
+ pred(3);
+ }
+ break;
+ }
+ }
+ }
+ setState(36);
+ _errHandler.sync(this);
+ _alt = getInterpreter().adaptivePredict(_input,3,_ctx);
+ }
+ }
+ }
+ catch (RecognitionException re) {
+ _localctx.exception = re;
+ _errHandler.reportError(this, re);
+ _errHandler.recover(this, re);
+ }
+ finally {
+ unrollRecursionContexts(_parentctx);
+ }
+ return _localctx;
+ }
+
+ @SuppressWarnings("CheckReturnValue")
+ public static class ExpContext extends ParserRuleContext {
+ public ExpContext(ParserRuleContext parent, int invokingState) {
+ super(parent, invokingState);
+ }
+ @Override public int getRuleIndex() { return RULE_exp; }
+
+ public ExpContext() { }
+ public void copyFrom(ExpContext ctx) {
+ super.copyFrom(ctx);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class ExpBoolContext extends ExpContext {
+ public List exp() {
+ return getRuleContexts(ExpContext.class);
+ }
+ public ExpContext exp(int i) {
+ return getRuleContext(ExpContext.class,i);
+ }
+ public TerminalNode BOOLOP() { return getToken(RefinementsLanguageParser.BOOLOP, 0); }
+ public ExpBoolContext(ExpContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterExpBool(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitExpBool(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitExpBool(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class ExpOperandContext extends ExpContext {
+ public OperandContext operand() {
+ return getRuleContext(OperandContext.class,0);
+ }
+ public ExpOperandContext(ExpContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterExpOperand(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitExpOperand(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitExpOperand(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class ExpGroupContext extends ExpContext {
+ public ExpContext exp() {
+ return getRuleContext(ExpContext.class,0);
+ }
+ public ExpGroupContext(ExpContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterExpGroup(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitExpGroup(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitExpGroup(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+
+ public final ExpContext exp() throws RecognitionException {
+ return exp(0);
+ }
+
+ private ExpContext exp(int _p) throws RecognitionException {
+ ParserRuleContext _parentctx = _ctx;
+ int _parentState = getState();
+ ExpContext _localctx = new ExpContext(_ctx, _parentState);
+ ExpContext _prevctx = _localctx;
+ int _startState = 4;
+ enterRecursionRule(_localctx, 4, RULE_exp, _p);
+ try {
+ int _alt;
+ enterOuterAlt(_localctx, 1);
+ {
+ setState(43);
+ _errHandler.sync(this);
+ switch ( getInterpreter().adaptivePredict(_input,4,_ctx) ) {
+ case 1:
+ {
+ _localctx = new ExpGroupContext(_localctx);
+ _ctx = _localctx;
+ _prevctx = _localctx;
+
+ setState(38);
+ match(T__0);
+ setState(39);
+ exp(0);
+ setState(40);
+ match(T__1);
+ }
+ break;
+ case 2:
+ {
+ _localctx = new ExpOperandContext(_localctx);
+ _ctx = _localctx;
+ _prevctx = _localctx;
+ setState(42);
+ operand(0);
+ }
+ break;
+ }
+ _ctx.stop = _input.LT(-1);
+ setState(50);
+ _errHandler.sync(this);
+ _alt = getInterpreter().adaptivePredict(_input,5,_ctx);
+ while ( _alt!=2 && _alt!=org.antlr.v4.runtime.atn.ATN.INVALID_ALT_NUMBER ) {
+ if ( _alt==1 ) {
+ if ( _parseListeners!=null ) triggerExitRuleEvent();
+ _prevctx = _localctx;
+ {
+ {
+ _localctx = new ExpBoolContext(new ExpContext(_parentctx, _parentState));
+ pushNewRecursionContext(_localctx, _startState, RULE_exp);
+ setState(45);
+ if (!(precpred(_ctx, 2))) throw new FailedPredicateException(this, "precpred(_ctx, 2)");
+ setState(46);
+ match(BOOLOP);
+ setState(47);
+ exp(3);
+ }
+ }
+ }
+ setState(52);
+ _errHandler.sync(this);
+ _alt = getInterpreter().adaptivePredict(_input,5,_ctx);
+ }
+ }
+ }
+ catch (RecognitionException re) {
+ _localctx.exception = re;
+ _errHandler.reportError(this, re);
+ _errHandler.recover(this, re);
+ }
+ finally {
+ unrollRecursionContexts(_parentctx);
+ }
+ return _localctx;
+ }
+
+ @SuppressWarnings("CheckReturnValue")
+ public static class OperandContext extends ParserRuleContext {
+ public OperandContext(ParserRuleContext parent, int invokingState) {
+ super(parent, invokingState);
+ }
+ @Override public int getRuleIndex() { return RULE_operand; }
+
+ public OperandContext() { }
+ public void copyFrom(OperandContext ctx) {
+ super.copyFrom(ctx);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class OpArithContext extends OperandContext {
+ public List operand() {
+ return getRuleContexts(OperandContext.class);
+ }
+ public OperandContext operand(int i) {
+ return getRuleContext(OperandContext.class,i);
+ }
+ public TerminalNode ARITHOP() { return getToken(RefinementsLanguageParser.ARITHOP, 0); }
+ public OpArithContext(OperandContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterOpArith(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitOpArith(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitOpArith(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class OpNotContext extends OperandContext {
+ public OperandContext operand() {
+ return getRuleContext(OperandContext.class,0);
+ }
+ public OpNotContext(OperandContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterOpNot(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitOpNot(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitOpNot(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class OpLiteralContext extends OperandContext {
+ public LeafsContext leafs() {
+ return getRuleContext(LeafsContext.class,0);
+ }
+ public OpLiteralContext(OperandContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterOpLiteral(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitOpLiteral(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitOpLiteral(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class OpGroupContext extends OperandContext {
+ public OperandContext operand() {
+ return getRuleContext(OperandContext.class,0);
+ }
+ public OpGroupContext(OperandContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterOpGroup(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitOpGroup(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitOpGroup(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class OpSubContext extends OperandContext {
+ public List operand() {
+ return getRuleContexts(OperandContext.class);
+ }
+ public OperandContext operand(int i) {
+ return getRuleContext(OperandContext.class,i);
+ }
+ public OpSubContext(OperandContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterOpSub(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitOpSub(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitOpSub(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+
+ public final OperandContext operand() throws RecognitionException {
+ return operand(0);
+ }
+
+ private OperandContext operand(int _p) throws RecognitionException {
+ ParserRuleContext _parentctx = _ctx;
+ int _parentState = getState();
+ OperandContext _localctx = new OperandContext(_ctx, _parentState);
+ OperandContext _prevctx = _localctx;
+ int _startState = 6;
+ enterRecursionRule(_localctx, 6, RULE_operand, _p);
+ try {
+ int _alt;
+ enterOuterAlt(_localctx, 1);
+ {
+ setState(61);
+ _errHandler.sync(this);
+ switch ( getInterpreter().adaptivePredict(_input,6,_ctx) ) {
+ case 1:
+ {
+ _localctx = new OpLiteralContext(_localctx);
+ _ctx = _localctx;
+ _prevctx = _localctx;
+
+ setState(54);
+ leafs();
+ }
+ break;
+ case 2:
+ {
+ _localctx = new OpNotContext(_localctx);
+ _ctx = _localctx;
+ _prevctx = _localctx;
+ setState(55);
+ match(T__2);
+ setState(56);
+ operand(2);
+ }
+ break;
+ case 3:
+ {
+ _localctx = new OpGroupContext(_localctx);
+ _ctx = _localctx;
+ _prevctx = _localctx;
+ setState(57);
+ match(T__0);
+ setState(58);
+ operand(0);
+ setState(59);
+ match(T__1);
+ }
+ break;
+ }
+ _ctx.stop = _input.LT(-1);
+ setState(71);
+ _errHandler.sync(this);
+ _alt = getInterpreter().adaptivePredict(_input,8,_ctx);
+ while ( _alt!=2 && _alt!=org.antlr.v4.runtime.atn.ATN.INVALID_ALT_NUMBER ) {
+ if ( _alt==1 ) {
+ if ( _parseListeners!=null ) triggerExitRuleEvent();
+ _prevctx = _localctx;
+ {
+ setState(69);
+ _errHandler.sync(this);
+ switch ( getInterpreter().adaptivePredict(_input,7,_ctx) ) {
+ case 1:
+ {
+ _localctx = new OpArithContext(new OperandContext(_parentctx, _parentState));
+ pushNewRecursionContext(_localctx, _startState, RULE_operand);
+ setState(63);
+ if (!(precpred(_ctx, 4))) throw new FailedPredicateException(this, "precpred(_ctx, 4)");
+ setState(64);
+ match(ARITHOP);
+ setState(65);
+ operand(5);
+ }
+ break;
+ case 2:
+ {
+ _localctx = new OpSubContext(new OperandContext(_parentctx, _parentState));
+ pushNewRecursionContext(_localctx, _startState, RULE_operand);
+ setState(66);
+ if (!(precpred(_ctx, 3))) throw new FailedPredicateException(this, "precpred(_ctx, 3)");
+ setState(67);
+ match(T__4);
+ setState(68);
+ operand(4);
+ }
+ break;
+ }
+ }
+ }
+ setState(73);
+ _errHandler.sync(this);
+ _alt = getInterpreter().adaptivePredict(_input,8,_ctx);
+ }
+ }
+ }
+ catch (RecognitionException re) {
+ _localctx.exception = re;
+ _errHandler.reportError(this, re);
+ _errHandler.recover(this, re);
+ }
+ finally {
+ unrollRecursionContexts(_parentctx);
+ }
+ return _localctx;
+ }
+
+ @SuppressWarnings("CheckReturnValue")
+ public static class LeafsContext extends ParserRuleContext {
+ public LeafsContext(ParserRuleContext parent, int invokingState) {
+ super(parent, invokingState);
+ }
+ @Override public int getRuleIndex() { return RULE_leafs; }
+
+ public LeafsContext() { }
+ public void copyFrom(LeafsContext ctx) {
+ super.copyFrom(ctx);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class TargetInvocationContext extends LeafsContext {
+ public List ID() { return getTokens(RefinementsLanguageParser.ID); }
+ public TerminalNode ID(int i) {
+ return getToken(RefinementsLanguageParser.ID, i);
+ }
+ public TargetInvocationContext(LeafsContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterTargetInvocation(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitTargetInvocation(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitTargetInvocation(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class LitGroupContext extends LeafsContext {
+ public LeafsContext leafs() {
+ return getRuleContext(LeafsContext.class,0);
+ }
+ public LitGroupContext(LeafsContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterLitGroup(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitLitGroup(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitLitGroup(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class LitContext extends LeafsContext {
+ public LiteralContext literal() {
+ return getRuleContext(LiteralContext.class,0);
+ }
+ public LitContext(LeafsContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterLit(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitLit(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitLit(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class VarContext extends LeafsContext {
+ public TerminalNode ID() { return getToken(RefinementsLanguageParser.ID, 0); }
+ public VarContext(LeafsContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterVar(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitVar(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitVar(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+
+ public final LeafsContext leafs() throws RecognitionException {
+ LeafsContext _localctx = new LeafsContext(_ctx, getState());
+ enterRule(_localctx, 8, RULE_leafs);
+ try {
+ setState(83);
+ _errHandler.sync(this);
+ switch ( getInterpreter().adaptivePredict(_input,9,_ctx) ) {
+ case 1:
+ _localctx = new LitGroupContext(_localctx);
+ enterOuterAlt(_localctx, 1);
+ {
+ setState(74);
+ match(T__0);
+ setState(75);
+ leafs();
+ setState(76);
+ match(T__1);
+ }
+ break;
+ case 2:
+ _localctx = new LitContext(_localctx);
+ enterOuterAlt(_localctx, 2);
+ {
+ setState(78);
+ literal();
+ }
+ break;
+ case 3:
+ _localctx = new VarContext(_localctx);
+ enterOuterAlt(_localctx, 3);
+ {
+ setState(79);
+ match(ID);
+ }
+ break;
+ case 4:
+ _localctx = new TargetInvocationContext(_localctx);
+ enterOuterAlt(_localctx, 4);
+ {
+ setState(80);
+ match(ID);
+ setState(81);
+ match(T__5);
+ setState(82);
+ match(ID);
+ }
+ break;
+ }
+ }
+ catch (RecognitionException re) {
+ _localctx.exception = re;
+ _errHandler.reportError(this, re);
+ _errHandler.recover(this, re);
+ }
+ finally {
+ exitRule();
+ }
+ return _localctx;
+ }
+
+ @SuppressWarnings("CheckReturnValue")
+ public static class LiteralContext extends ParserRuleContext {
+ public LiteralContext(ParserRuleContext parent, int invokingState) {
+ super(parent, invokingState);
+ }
+ @Override public int getRuleIndex() { return RULE_literal; }
+
+ public LiteralContext() { }
+ public void copyFrom(LiteralContext ctx) {
+ super.copyFrom(ctx);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class LitIntContext extends LiteralContext {
+ public TerminalNode INT() { return getToken(RefinementsLanguageParser.INT, 0); }
+ public LitIntContext(LiteralContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterLitInt(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitLitInt(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitLitInt(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+ @SuppressWarnings("CheckReturnValue")
+ public static class LitBoolContext extends LiteralContext {
+ public TerminalNode BOOL() { return getToken(RefinementsLanguageParser.BOOL, 0); }
+ public LitBoolContext(LiteralContext ctx) { copyFrom(ctx); }
+ @Override
+ public void enterRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).enterLitBool(this);
+ }
+ @Override
+ public void exitRule(ParseTreeListener listener) {
+ if ( listener instanceof RefinementsLanguageListener ) ((RefinementsLanguageListener)listener).exitLitBool(this);
+ }
+ @Override
+ public T accept(ParseTreeVisitor visitor) {
+ if ( visitor instanceof RefinementsLanguageVisitor ) return ((RefinementsLanguageVisitor)visitor).visitLitBool(this);
+ else return visitor.visitChildren(this);
+ }
+ }
+
+ public final LiteralContext literal() throws RecognitionException {
+ LiteralContext _localctx = new LiteralContext(_ctx, getState());
+ enterRule(_localctx, 10, RULE_literal);
+ try {
+ setState(87);
+ _errHandler.sync(this);
+ switch (_input.LA(1)) {
+ case BOOL:
+ _localctx = new LitBoolContext(_localctx);
+ enterOuterAlt(_localctx, 1);
+ {
+ setState(85);
+ match(BOOL);
+ }
+ break;
+ case INT:
+ _localctx = new LitIntContext(_localctx);
+ enterOuterAlt(_localctx, 2);
+ {
+ setState(86);
+ match(INT);
+ }
+ break;
+ default:
+ throw new NoViableAltException(this);
+ }
+ }
+ catch (RecognitionException re) {
+ _localctx.exception = re;
+ _errHandler.reportError(this, re);
+ _errHandler.recover(this, re);
+ }
+ finally {
+ exitRule();
+ }
+ return _localctx;
+ }
+
+ public boolean sempred(RuleContext _localctx, int ruleIndex, int predIndex) {
+ switch (ruleIndex) {
+ case 1:
+ return pred_sempred((PredContext)_localctx, predIndex);
+ case 2:
+ return exp_sempred((ExpContext)_localctx, predIndex);
+ case 3:
+ return operand_sempred((OperandContext)_localctx, predIndex);
+ }
+ return true;
+ }
+ private boolean pred_sempred(PredContext _localctx, int predIndex) {
+ switch (predIndex) {
+ case 0:
+ return precpred(_ctx, 3);
+ case 1:
+ return precpred(_ctx, 2);
+ }
+ return true;
+ }
+ private boolean exp_sempred(ExpContext _localctx, int predIndex) {
+ switch (predIndex) {
+ case 2:
+ return precpred(_ctx, 2);
+ }
+ return true;
+ }
+ private boolean operand_sempred(OperandContext _localctx, int predIndex) {
+ switch (predIndex) {
+ case 3:
+ return precpred(_ctx, 4);
+ case 4:
+ return precpred(_ctx, 3);
+ }
+ return true;
+ }
+
+ public static final String _serializedATN =
+ "\u0004\u0001\u000eZ\u0002\u0000\u0007\u0000\u0002\u0001\u0007\u0001\u0002"+
+ "\u0002\u0007\u0002\u0002\u0003\u0007\u0003\u0002\u0004\u0007\u0004\u0002"+
+ "\u0005\u0007\u0005\u0001\u0000\u0001\u0000\u0003\u0000\u000f\b\u0000\u0001"+
+ "\u0001\u0001\u0001\u0001\u0001\u0001\u0001\u0001\u0001\u0001\u0001\u0001"+
+ "\u0001\u0001\u0001\u0003\u0001\u0019\b\u0001\u0001\u0001\u0001\u0001\u0001"+
+ "\u0001\u0001\u0001\u0001\u0001\u0001\u0001\u0005\u0001!\b\u0001\n\u0001"+
+ "\f\u0001$\t\u0001\u0001\u0002\u0001\u0002\u0001\u0002\u0001\u0002\u0001"+
+ "\u0002\u0001\u0002\u0003\u0002,\b\u0002\u0001\u0002\u0001\u0002\u0001"+
+ "\u0002\u0005\u00021\b\u0002\n\u0002\f\u00024\t\u0002\u0001\u0003\u0001"+
+ "\u0003\u0001\u0003\u0001\u0003\u0001\u0003\u0001\u0003\u0001\u0003\u0001"+
+ "\u0003\u0003\u0003>\b\u0003\u0001\u0003\u0001\u0003\u0001\u0003\u0001"+
+ "\u0003\u0001\u0003\u0001\u0003\u0005\u0003F\b\u0003\n\u0003\f\u0003I\t"+
+ "\u0003\u0001\u0004\u0001\u0004\u0001\u0004\u0001\u0004\u0001\u0004\u0001"+
+ "\u0004\u0001\u0004\u0001\u0004\u0001\u0004\u0003\u0004T\b\u0004\u0001"+
+ "\u0005\u0001\u0005\u0003\u0005X\b\u0005\u0001\u0005\u0000\u0003\u0002"+
+ "\u0004\u0006\u0006\u0000\u0002\u0004\u0006\b\n\u0000\u0000b\u0000\u000e"+
+ "\u0001\u0000\u0000\u0000\u0002\u0018\u0001\u0000\u0000\u0000\u0004+\u0001"+
+ "\u0000\u0000\u0000\u0006=\u0001\u0000\u0000\u0000\bS\u0001\u0000\u0000"+
+ "\u0000\nW\u0001\u0000\u0000\u0000\f\u000f\u0003\u0002\u0001\u0000\r\u000f"+
+ "\u0001\u0000\u0000\u0000\u000e\f\u0001\u0000\u0000\u0000\u000e\r\u0001"+
+ "\u0000\u0000\u0000\u000f\u0001\u0001\u0000\u0000\u0000\u0010\u0011\u0006"+
+ "\u0001\uffff\uffff\u0000\u0011\u0012\u0005\u0001\u0000\u0000\u0012\u0013"+
+ "\u0003\u0002\u0001\u0000\u0013\u0014\u0005\u0002\u0000\u0000\u0014\u0019"+
+ "\u0001\u0000\u0000\u0000\u0015\u0016\u0005\u0003\u0000\u0000\u0016\u0019"+
+ "\u0003\u0002\u0001\u0004\u0017\u0019\u0003\u0004\u0002\u0000\u0018\u0010"+
+ "\u0001\u0000\u0000\u0000\u0018\u0015\u0001\u0000\u0000\u0000\u0018\u0017"+
+ "\u0001\u0000\u0000\u0000\u0019\"\u0001\u0000\u0000\u0000\u001a\u001b\n"+
+ "\u0003\u0000\u0000\u001b\u001c\u0005\u0007\u0000\u0000\u001c!\u0003\u0002"+
+ "\u0001\u0004\u001d\u001e\n\u0002\u0000\u0000\u001e\u001f\u0005\u0004\u0000"+
+ "\u0000\u001f!\u0003\u0002\u0001\u0003 \u001a\u0001\u0000\u0000\u0000 "+
+ "\u001d\u0001\u0000\u0000\u0000!$\u0001\u0000\u0000\u0000\" \u0001\u0000"+
+ "\u0000\u0000\"#\u0001\u0000\u0000\u0000#\u0003\u0001\u0000\u0000\u0000"+
+ "$\"\u0001\u0000\u0000\u0000%&\u0006\u0002\uffff\uffff\u0000&\'\u0005\u0001"+
+ "\u0000\u0000\'(\u0003\u0004\u0002\u0000()\u0005\u0002\u0000\u0000),\u0001"+
+ "\u0000\u0000\u0000*,\u0003\u0006\u0003\u0000+%\u0001\u0000\u0000\u0000"+
+ "+*\u0001\u0000\u0000\u0000,2\u0001\u0000\u0000\u0000-.\n\u0002\u0000\u0000"+
+ "./\u0005\b\u0000\u0000/1\u0003\u0004\u0002\u00030-\u0001\u0000\u0000\u0000"+
+ "14\u0001\u0000\u0000\u000020\u0001\u0000\u0000\u000023\u0001\u0000\u0000"+
+ "\u00003\u0005\u0001\u0000\u0000\u000042\u0001\u0000\u0000\u000056\u0006"+
+ "\u0003\uffff\uffff\u00006>\u0003\b\u0004\u000078\u0005\u0003\u0000\u0000"+
+ "8>\u0003\u0006\u0003\u00029:\u0005\u0001\u0000\u0000:;\u0003\u0006\u0003"+
+ "\u0000;<\u0005\u0002\u0000\u0000<>\u0001\u0000\u0000\u0000=5\u0001\u0000"+
+ "\u0000\u0000=7\u0001\u0000\u0000\u0000=9\u0001\u0000\u0000\u0000>G\u0001"+
+ "\u0000\u0000\u0000?@\n\u0004\u0000\u0000@A\u0005\t\u0000\u0000AF\u0003"+
+ "\u0006\u0003\u0005BC\n\u0003\u0000\u0000CD\u0005\u0005\u0000\u0000DF\u0003"+
+ "\u0006\u0003\u0004E?\u0001\u0000\u0000\u0000EB\u0001\u0000\u0000\u0000"+
+ "FI\u0001\u0000\u0000\u0000GE\u0001\u0000\u0000\u0000GH\u0001\u0000\u0000"+
+ "\u0000H\u0007\u0001\u0000\u0000\u0000IG\u0001\u0000\u0000\u0000JK\u0005"+
+ "\u0001\u0000\u0000KL\u0003\b\u0004\u0000LM\u0005\u0002\u0000\u0000MT\u0001"+
+ "\u0000\u0000\u0000NT\u0003\n\u0005\u0000OT\u0005\f\u0000\u0000PQ\u0005"+
+ "\f\u0000\u0000QR\u0005\u0006\u0000\u0000RT\u0005\f\u0000\u0000SJ\u0001"+
+ "\u0000\u0000\u0000SN\u0001\u0000\u0000\u0000SO\u0001\u0000\u0000\u0000"+
+ "SP\u0001\u0000\u0000\u0000T\t\u0001\u0000\u0000\u0000UX\u0005\n\u0000"+
+ "\u0000VX\u0005\r\u0000\u0000WU\u0001\u0000\u0000\u0000WV\u0001\u0000\u0000"+
+ "\u0000X\u000b\u0001\u0000\u0000\u0000\u000b\u000e\u0018 \"+2=EGSW";
+ public static final ATN _ATN =
+ new ATNDeserializer().deserialize(_serializedATN.toCharArray());
+ static {
+ _decisionToDFA = new DFA[_ATN.getNumberOfDecisions()];
+ for (int i = 0; i < _ATN.getNumberOfDecisions(); i++) {
+ _decisionToDFA[i] = new DFA(_ATN.getDecisionState(i), i);
+ }
+ }
+}
\ No newline at end of file
diff --git a/latte/src/main/java/refinements/RefinementsLanguageVisitor.java b/latte/src/main/java/refinements/RefinementsLanguageVisitor.java
new file mode 100644
index 0000000..e83650c
--- /dev/null
+++ b/latte/src/main/java/refinements/RefinementsLanguageVisitor.java
@@ -0,0 +1,152 @@
+// Generated from RefinementsLanguage.g4 by ANTLR 4.13.1
+package refinements;
+import org.antlr.v4.runtime.tree.ParseTreeVisitor;
+
+/**
+ * This interface defines a complete generic visitor for a parse tree produced
+ * by {@link RefinementsLanguageParser}.
+ *
+ * @param The return type of the visit operation. Use {@link Void} for
+ * operations with no return type.
+ */
+public interface RefinementsLanguageVisitor extends ParseTreeVisitor {
+ /**
+ * Visit a parse tree produced by {@link RefinementsLanguageParser#prog}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitProg(RefinementsLanguageParser.ProgContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code predGroup}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitPredGroup(RefinementsLanguageParser.PredGroupContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code predNegate}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitPredNegate(RefinementsLanguageParser.PredNegateContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code predExp}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitPredExp(RefinementsLanguageParser.PredExpContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code predImplies}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitPredImplies(RefinementsLanguageParser.PredImpliesContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code predLogic}
+ * labeled alternative in {@link RefinementsLanguageParser#pred}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitPredLogic(RefinementsLanguageParser.PredLogicContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code expBool}
+ * labeled alternative in {@link RefinementsLanguageParser#exp}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitExpBool(RefinementsLanguageParser.ExpBoolContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code expOperand}
+ * labeled alternative in {@link RefinementsLanguageParser#exp}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitExpOperand(RefinementsLanguageParser.ExpOperandContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code expGroup}
+ * labeled alternative in {@link RefinementsLanguageParser#exp}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitExpGroup(RefinementsLanguageParser.ExpGroupContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code opArith}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitOpArith(RefinementsLanguageParser.OpArithContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code opNot}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitOpNot(RefinementsLanguageParser.OpNotContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code opLiteral}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitOpLiteral(RefinementsLanguageParser.OpLiteralContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code opGroup}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitOpGroup(RefinementsLanguageParser.OpGroupContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code opSub}
+ * labeled alternative in {@link RefinementsLanguageParser#operand}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitOpSub(RefinementsLanguageParser.OpSubContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code litGroup}
+ * labeled alternative in {@link RefinementsLanguageParser#leafs}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitLitGroup(RefinementsLanguageParser.LitGroupContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code lit}
+ * labeled alternative in {@link RefinementsLanguageParser#leafs}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitLit(RefinementsLanguageParser.LitContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code var}
+ * labeled alternative in {@link RefinementsLanguageParser#leafs}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitVar(RefinementsLanguageParser.VarContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code targetInvocation}
+ * labeled alternative in {@link RefinementsLanguageParser#leafs}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitTargetInvocation(RefinementsLanguageParser.TargetInvocationContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code litBool}
+ * labeled alternative in {@link RefinementsLanguageParser#literal}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitLitBool(RefinementsLanguageParser.LitBoolContext ctx);
+ /**
+ * Visit a parse tree produced by the {@code litInt}
+ * labeled alternative in {@link RefinementsLanguageParser#literal}.
+ * @param ctx the parse tree
+ * @return the visitor result
+ */
+ T visitLitInt(RefinementsLanguageParser.LitIntContext ctx);
+}
\ No newline at end of file
diff --git a/latte/src/main/java/refinements/TestRefinementsLanguage.java b/latte/src/main/java/refinements/TestRefinementsLanguage.java
new file mode 100644
index 0000000..fe2c046
--- /dev/null
+++ b/latte/src/main/java/refinements/TestRefinementsLanguage.java
@@ -0,0 +1,39 @@
+package refinements;
+
+import org.antlr.v4.runtime.CharStream;
+import org.antlr.v4.runtime.CharStreams;
+import org.antlr.v4.runtime.CommonTokenStream;
+import org.antlr.v4.runtime.tree.ParseTree;
+
+/**
+ * Test class for the Refinements Language parser.
+ * This class demonstrates how to parse a simple expression using ANTLR.
+ */
+public class TestRefinementsLanguage {
+
+ public static void main(String[] args) {
+ String input = "10";
+
+ // // Create input stream (modern way)
+ CharStream inputStream = CharStreams.fromString(input);
+
+ // Create lexer
+ RefinementsLanguageLexer lexer = new RefinementsLanguageLexer(inputStream);
+
+ // Create token stream
+ CommonTokenStream tokens = new CommonTokenStream(lexer);
+
+ // Create parser
+ RefinementsLanguageParser parser = new RefinementsLanguageParser(tokens);
+
+ // Parse starting from your grammar's start rule
+ // Replace 'program' with your actual start rule name
+ ParseTree tree = parser.prog(); // Change 'program' to your start rule
+
+ // Print the parse tree
+ System.out.println("Parse Tree:");
+ System.out.println(tree.toStringTree(parser));
+
+ }
+
+}
diff --git a/latte/src/main/java/smt/JavaSMTTest.java b/latte/src/main/java/smt/JavaSMTTest.java
new file mode 100644
index 0000000..296dff5
--- /dev/null
+++ b/latte/src/main/java/smt/JavaSMTTest.java
@@ -0,0 +1,138 @@
+package smt;
+
+import com.microsoft.z3.*;
+
+/**
+ * Simple Java program to test Z3 SMT solver with a specific implication.
+ */
+public class JavaSMTTest {
+ public static void main(String[] args) {
+ System.out.println("Testing Z3 Turnkey (with bundled natives)...");
+
+ try {
+ // Test the specific query: x == 0 -> x > -1
+ testImplication();
+
+ } catch (Exception e) {
+ System.err.println("Error: " + e.getMessage());
+ e.printStackTrace();
+ }
+ }
+
+ public static void testImplication() {
+ System.out.println("Checking: x == 0 -> x > -1");
+ // Translation to z3 of the expression above is the following:
+
+ try (Context ctx = new Context()) {
+
+ // Create integer variable x
+ IntExpr x = ctx.mkIntConst("x");
+
+ // Create the expressions
+ BoolExpr xEquals0 = ctx.mkEq(x, ctx.mkInt(0)); // x == 0
+ BoolExpr xGreaterThanMinus1 = ctx.mkGt(x, ctx.mkInt(-1)); // x > -1
+
+ // Create the implication: x == 0 -> x > -1
+ BoolExpr implication = ctx.mkImplies(xEquals0, xGreaterThanMinus1);
+
+ // Create solver
+ Solver solver = ctx.mkSolver();
+
+ // Check if implication is valid (tautology)
+ // We do this by checking if the negation is unsatisfiable
+ solver.add(ctx.mkNot(implication));
+
+ Status result = solver.check();
+
+ System.out.println("Result: " + result);
+
+ if (result == Status.UNSATISFIABLE) {
+ System.out.println("β VALID: The implication x == 0 -> x > -1 is always true");
+ } else if (result == Status.SATISFIABLE) {
+ System.out.println("β INVALID: Found a counterexample");
+ Model model = solver.getModel();
+ System.out.println("Counterexample: x = " + model.evaluate(x, false));
+ } else {
+ System.out.println("? UNKNOWN");
+ }
+
+ // Also test satisfiability of the implication itself
+ System.out.println("\nTesting satisfiability of the implication...");
+ Solver solver2 = ctx.mkSolver();
+ solver2.add(implication);
+
+ Status sat_result = solver2.check();
+ System.out.println("Satisfiability: " + sat_result);
+
+ if (sat_result == Status.SATISFIABLE) {
+ Model model = solver2.getModel();
+ System.out.println("Example where implication holds: x = " + model.evaluate(x, false));
+ }
+
+ } catch (Exception e) {
+ System.err.println("Error in test: " + e.getMessage());
+ e.printStackTrace();
+ }
+ }
+
+ // Test multiple implications
+ public static void testMultipleImplications() {
+ System.out.println("\n=== Testing Multiple Implications ===");
+
+ String[] queries = {
+ "x == 0 -> x > -1",
+ "x > 5 -> x > 0",
+ "x == 0 -> x < 0"
+ };
+
+ for (String query : queries) {
+ System.out.println("\nTesting: " + query);
+ boolean result = checkImplication(query);
+ System.out.println("Result: " + (result ? "VALID" : "INVALID"));
+ }
+ }
+
+ private static boolean checkImplication(String description) {
+ try (Context ctx = new Context()) {
+ IntExpr x = ctx.mkIntConst("x");
+ BoolExpr implication = null;
+
+ // Build specific implications
+ if (description.contains("x == 0 -> x > -1")) {
+ implication = ctx.mkImplies(
+ ctx.mkEq(x, ctx.mkInt(0)),
+ ctx.mkGt(x, ctx.mkInt(-1))
+ );
+ } else if (description.contains("x > 5 -> x > 0")) {
+ implication = ctx.mkImplies(
+ ctx.mkGt(x, ctx.mkInt(5)),
+ ctx.mkGt(x, ctx.mkInt(0))
+ );
+ } else if (description.contains("x == 0 -> x < 0")) {
+ implication = ctx.mkImplies(
+ ctx.mkEq(x, ctx.mkInt(0)),
+ ctx.mkLt(x, ctx.mkInt(0))
+ );
+ }
+
+ if (implication == null) return false;
+
+ Solver solver = ctx.mkSolver();
+ solver.add(ctx.mkNot(implication));
+
+ Status result = solver.check();
+
+ if (result == Status.SATISFIABLE) {
+ Model model = solver.getModel();
+ System.out.println(" Counterexample: x = " + model.evaluate(x, false));
+ return false;
+ }
+
+ return result == Status.UNSATISFIABLE;
+
+ } catch (Exception e) {
+ System.err.println("Error: " + e.getMessage());
+ return false;
+ }
+ }
+}
\ No newline at end of file
diff --git a/latte/src/main/java/smt/RefinementsToZ3Translator.java b/latte/src/main/java/smt/RefinementsToZ3Translator.java
new file mode 100644
index 0000000..1b6744b
--- /dev/null
+++ b/latte/src/main/java/smt/RefinementsToZ3Translator.java
@@ -0,0 +1,208 @@
+package smt;
+
+import org.antlr.v4.runtime.tree.ParseTree;
+
+import com.microsoft.z3.*;
+
+import refinements.*;
+import refinements.RefinementsLanguageParser.ProgContext;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ * The translator extends RefinementsLanguageBaseVisitor and converts parse tree nodes
+ * to Z3 Expr objects (BoolExpr for boolean expressions, ArithExpr for arithmetic, etc.)
+ */
+public class RefinementsToZ3Translator extends RefinementsLanguageBaseVisitor {
+ private final Context z3Context;
+ private final Map variableMap;
+
+ public RefinementsToZ3Translator(Context z3Context) {
+ this.z3Context = z3Context;
+ this.variableMap = new HashMap<>();
+ }
+
+ /**
+ * Main entry point - translate a parse tree to a Z3 formula
+ * This method is already complete.
+ */
+ public Expr translate(ParseTree tree) {
+ Expr result = visit(tree);
+ if (result != null) {
+ return result;
+ } else {
+ throw new IllegalArgumentException("Root expression must be expression, got: " + result.getClass());
+ }
+ }
+
+ @Override
+ public Expr visitProg(ProgContext ctx) {
+ return super.visitProg(ctx);
+ }
+
+ // =================================================================
+ // Implement visitor methods for elements in the grammar
+ // =================================================================
+
+ @Override
+ public Expr visitLitBool(RefinementsLanguageParser.LitBoolContext ctx) {
+ if (ctx.getText().equals("true")) {
+ return z3Context.mkTrue();
+ } else {
+ return z3Context.mkFalse();
+ }
+ }
+
+ @Override
+ public Expr visitLitInt(RefinementsLanguageParser.LitIntContext ctx) {
+ String intText = ctx.getText().replace("_", ""); // sanitize e.g., 1_000
+ int value = Integer.parseInt(intText);
+ return z3Context.mkInt(value);
+ }
+
+ @Override
+ public Expr visitLit(RefinementsLanguageParser.LitContext ctx) {
+ return visit(ctx.literal()); // Delegate to litBool or litInt
+ }
+
+ @Override
+ public Expr visitVar(RefinementsLanguageParser.VarContext ctx) {
+ String varName = ctx.getText();
+
+ // Look up if we've already created a Z3 variable for this name
+ if (variableMap.containsKey(varName)) {
+ return variableMap.get(varName);
+ }
+
+ // If not, create a fresh Z3 integer variable (default assumption)
+ // Later you could refine this to support booleans too if needed.
+ Expr z3Var = z3Context.mkIntConst(varName);
+
+ // Store it in the map so itβs reused consistently
+ variableMap.put(varName, z3Var);
+
+ return z3Var;
+ }
+
+ @Override
+ public Expr visitOpArith(RefinementsLanguageParser.OpArithContext ctx) {
+ // Visit the left and right operands
+ Expr left = visit(ctx.operand(0));
+ Expr right = visit(ctx.operand(1));
+ String op = ctx.ARITHOP().getText();
+
+ // Ensure both sides are arithmetic expressions
+ if (!(left instanceof ArithExpr) || !(right instanceof ArithExpr)) {
+ throw new IllegalArgumentException("Operands must be arithmetic expressions");
+ }
+
+ ArithExpr leftArith = (ArithExpr) left;
+ ArithExpr rightArith = (ArithExpr) right;
+
+ // Dispatch based on operator
+ switch (op) {
+ case "+":
+ return z3Context.mkAdd(leftArith, rightArith);
+ case "*":
+ return z3Context.mkMul(leftArith, rightArith);
+ case "/":
+ return z3Context.mkDiv(leftArith, rightArith); // Integer division
+ default:
+ throw new UnsupportedOperationException("Unknown arithmetic operator: " + op);
+ }
+ }
+
+ @Override
+ public Expr visitExpBool(RefinementsLanguageParser.ExpBoolContext ctx) {
+ Expr left = visit(ctx.exp(0));
+ Expr right = visit(ctx.exp(1));
+ String op = ctx.BOOLOP().getText();
+
+ if (!(left instanceof ArithExpr) || !(right instanceof ArithExpr)) {
+ throw new IllegalArgumentException("Both sides of a comparison must be arithmetic expressions.");
+ }
+
+ ArithExpr leftArith = (ArithExpr) left;
+ ArithExpr rightArith = (ArithExpr) right;
+
+ switch (op) {
+ case "==":
+ return z3Context.mkEq(leftArith, rightArith);
+ case "<":
+ return z3Context.mkLt(leftArith, rightArith);
+ case "<=":
+ return z3Context.mkLe(leftArith, rightArith);
+ case ">":
+ return z3Context.mkGt(leftArith, rightArith);
+ case ">=":
+ return z3Context.mkGe(leftArith, rightArith);
+ default:
+ throw new UnsupportedOperationException("Unknown boolean operator: " + op);
+ }
+ }
+
+ @Override
+ public Expr visitPredNegate(RefinementsLanguageParser.PredNegateContext ctx) {
+ Expr inner = visit(ctx.pred());
+ if (!(inner instanceof BoolExpr)) {
+ throw new IllegalArgumentException("Negation requires a boolean expression.");
+ }
+ return z3Context.mkNot((BoolExpr) inner);
+ }
+
+ @Override
+ public Expr visitPredLogic(RefinementsLanguageParser.PredLogicContext ctx) {
+ Expr left = visit(ctx.pred(0));
+ Expr right = visit(ctx.pred(1));
+ String op = ctx.LOGOP().getText();
+
+ if (!(left instanceof BoolExpr) || !(right instanceof BoolExpr)) {
+ throw new IllegalArgumentException("Logical operations require boolean expressions.");
+ }
+
+ BoolExpr leftBool = (BoolExpr) left;
+ BoolExpr rightBool = (BoolExpr) right;
+
+ switch (op) {
+ case "&&":
+ return z3Context.mkAnd(leftBool, rightBool);
+ case "||":
+ return z3Context.mkOr(leftBool, rightBool);
+ default:
+ throw new UnsupportedOperationException("Unknown logical operator: " + op);
+ }
+ }
+
+ @Override
+ public Expr visitPredImplies(RefinementsLanguageParser.PredImpliesContext ctx) {
+ Expr left = visit(ctx.pred(0));
+ Expr right = visit(ctx.pred(1));
+
+ if (!(left instanceof BoolExpr) || !(right instanceof BoolExpr)) {
+ throw new IllegalArgumentException("Implication requires boolean expressions.");
+ }
+
+ return z3Context.mkImplies((BoolExpr) left, (BoolExpr) right);
+ }
+
+ @Override
+ public Expr visitExpGroup(RefinementsLanguageParser.ExpGroupContext ctx) {
+ return visit(ctx.exp());
+ }
+
+ @Override
+ public Expr visitPredGroup(RefinementsLanguageParser.PredGroupContext ctx) {
+ return visit(ctx.pred());
+ }
+
+ @Override
+ public Expr visitOpGroup(RefinementsLanguageParser.OpGroupContext ctx) {
+ return visit(ctx.operand());
+ }
+
+ @Override
+ public Expr visitLitGroup(RefinementsLanguageParser.LitGroupContext ctx) {
+ return visit(ctx.leafs());
+ }
+}
\ No newline at end of file
diff --git a/latte/src/main/java/smt/SimpleTranslatorTest.java b/latte/src/main/java/smt/SimpleTranslatorTest.java
new file mode 100644
index 0000000..5675228
--- /dev/null
+++ b/latte/src/main/java/smt/SimpleTranslatorTest.java
@@ -0,0 +1,238 @@
+package smt;
+
+import org.antlr.v4.runtime.*;
+import org.antlr.v4.runtime.tree.*;
+
+import com.microsoft.z3.*;
+
+import refinements.*;
+
+/**
+ * Test class to verify RefinementsToZ3Translator implementation
+ *
+ * Run this class after implementing methods in the translator.
+ * Start with simple tests and work your way up to complex ones.
+ */
+public class SimpleTranslatorTest {
+
+ public static void main(String[] args) {
+ System.out.println("Testing Student Translator Implementation");
+ System.out.println("========================================");
+
+ // Test in order of difficulty
+ testStep1_Literals();
+ testStep2_Variables();
+ testStep3_Arithmetic();
+ testStep4_Comparisons();
+ testStep5_LogicalOperations();
+ testStep6_Implications();
+ testStep7_ComplexExpressions();
+ }
+
+ public static void testStep1_Literals() {
+ System.out.println("\nπΈ STEP 1: Testing Literals");
+ System.out.println("Implement: visitIntegerLiteral, visitBooleanLiteral");
+
+ testExpression("5", "Should create Z3 integer 5");
+ testExpression("42", "Should create Z3 integer 42");
+ testExpression("true", "Should create Z3 true");
+ testExpression("false", "Should create Z3 false");
+ }
+
+ public static void testStep2_Variables() {
+ System.out.println("\nπΈ STEP 2: Testing Variables");
+ System.out.println("Implement: visitVariable");
+
+ testExpression("x", "Should create Z3 variable x");
+ testExpression("myVar", "Should create Z3 variable myVar");
+ }
+
+ public static void testStep3_Arithmetic() {
+ System.out.println("\nπΈ STEP 3: Testing Arithmetic");
+ System.out.println("Implement: visitArithmetic");
+
+ testExpression("x + 5", "Should create addition");
+ testExpression("10 - y", "Should create subtraction");
+ testExpression("x * 2", "Should create multiplication");
+ }
+
+ public static void testStep4_Comparisons() {
+ System.out.println("\nπΈ STEP 4: Testing Comparisons");
+ System.out.println("Implement: visitEquality, visitRelational");
+
+ testExpression("x == 5", "Should create equality");
+ testExpression("x > 0", "Should create greater than");
+ testExpression("y >= 10", "Should create greater or equal");
+ testExpression("z < 0", "Should create less than");
+ testExpression("w <= 5", "Should create less or equal");
+ }
+
+ public static void testStep5_LogicalOperations() {
+ System.out.println("\nπΈ STEP 5: Testing Logical Operations");
+ System.out.println("Implement: visitLogicalAnd, visitLogicalOr, visitLogicalNot");
+
+ testExpression("x > 0 && y < 5", "Should create logical AND");
+ testExpression("x == 0 || y == 0", "Should create logical OR");
+ testExpression("!x > 0", "Should create logical NOT");
+ }
+
+ public static void testStep6_Implications() {
+ System.out.println("\nπΈ STEP 6: Testing Implications");
+ System.out.println("Implement: visitImplication");
+
+ testExpression("x == 0 -> x <= 1", "Should create implication");
+ testExpression("x > 5 -> x > 0", "Should create implication");
+ }
+
+ public static void testStep7_ComplexExpressions() {
+ System.out.println("\nπΈ STEP 7: Testing Complex Expressions");
+ System.out.println("All methods should work together");
+
+ testExpression("(x > 0 && y > 0) -> (x + y > 0)", "Complex implication");
+ testExpression("x == 0 -> (x > (0 - 1) && x < 1)", "Implication with AND");
+ testExpression("(x + y == 10) && (x > y)", "Conjunction of constraints");
+ }
+
+ /**
+ * Test a single expression and report results
+ */
+ private static void testExpression(String expression, String description) {
+ System.out.print(" Testing: " + expression + " (" + description + ") ... ");
+
+ try (Context ctx = new Context()) {
+
+ // Try to translate the expression
+ Expr result = translateExpression(expression, ctx);
+
+ if (result != null) {
+ System.out.println("β
SUCCESS");
+ System.out.println(" Z3 Formula: " + result + ": " + result.getClass().getSimpleName());
+
+ // For non-tautologies, try to find a model
+ if (!expression.contains("->")) {
+ tryFindModel(result, ctx);
+ }
+ } else {
+ System.out.println("β FAILED - Could not translate");
+ }
+
+ } catch (UnsupportedOperationException e) {
+ System.out.println("β³ TODO - " + e.getMessage());
+ } catch (Exception e) {
+ System.out.println("β ERROR - " + e.getMessage());
+ }
+ }
+
+ /**
+ * Translate expression using student's implementation
+ */
+ private static Expr translateExpression(String expression, Context ctx) {
+ try {
+ // Parse with ANTLR
+ CharStream input = CharStreams.fromString(expression);
+ RefinementsLanguageLexer lexer = new RefinementsLanguageLexer(input);
+ CommonTokenStream tokens = new CommonTokenStream(lexer);
+ RefinementsLanguageParser parser = new RefinementsLanguageParser(tokens);
+
+ // Error handling
+ parser.removeErrorListeners();
+ parser.addErrorListener(new BaseErrorListener() {
+ @Override
+ public void syntaxError(Recognizer recognizer, Object offendingSymbol,
+ int line, int charPositionInLine, String msg, RecognitionException e) {
+ throw new RuntimeException("Parse error: " + msg);
+ }
+ });
+
+ // Parse
+ ParseTree tree = parser.prog();
+ System.out.println("\n Parse Tree: " + tree.toStringTree(parser));
+
+ // Translate using student's implementation
+ RefinementsToZ3Translator translator = new RefinementsToZ3Translator(ctx);
+ return translator.translate(tree);
+
+ } catch (Exception e) {
+ throw new RuntimeException("Translation failed: " + e.getMessage(), e);
+ }
+ }
+
+ /**
+ * Try to find a satisfying model for the expression
+ */
+ private static void tryFindModel(Expr formula, Context ctx) {
+ try {
+ Solver solver = ctx.mkSolver();
+ solver.add(formula);
+
+ System.out.println("Translation to SMT:\n"+solver.toString());
+ Status result = solver.check();
+
+ if (result == Status.SATISFIABLE) {
+ Model model = solver.getModel();
+ System.out.println(" Example solution: " + getModelString(model));
+ } else if (result == Status.UNSATISFIABLE) {
+ System.out.println(" (Unsatisfiable - no solutions exist)");
+ }
+
+ } catch (Exception e) {
+ // Ignore model-finding errors
+ }
+ }
+
+ /**
+ * Convert model to readable string
+ */
+ private static String getModelString(Model model) {
+ StringBuilder sb = new StringBuilder();
+ FuncDecl[] decls = model.getDecls();
+
+ for (int i = 0; i < decls.length; i++) {
+ if (i > 0) sb.append(", ");
+ String name = decls[i].getName().toString();
+ Expr value = model.getConstInterp(decls[i]);
+ sb.append(name).append("=").append(value);
+ }
+
+ return sb.toString();
+ }
+
+ /**
+ * Bonus: Test validity of implications
+ */
+ public static void testValidityCheck() {
+ System.out.println("\nπΈ BONUS: Testing Validity Checking");
+
+ String[] implications = {
+ "x == 0 -> x > -1", // Should be valid
+ "x > 5 -> x > 0", // Should be valid
+ "x == 0 -> x < 0" // Should be invalid
+ };
+
+ for (String impl : implications) {
+ System.out.print(" Checking validity of: " + impl + " ... ");
+
+ try (Context ctx = new Context()) {
+ Expr formula = translateExpression(impl, ctx);
+
+ if (formula != null) {
+ Solver solver = ctx.mkSolver();
+ solver.add(ctx.mkNot(formula)); // Negate to check validity
+
+ Status result = solver.check();
+
+ if (result == Status.UNSATISFIABLE) {
+ System.out.println("β
VALID (always true)");
+ } else {
+ System.out.println("β INVALID (counterexample exists)");
+ }
+ } else {
+ System.out.println("β Could not translate");
+ }
+
+ } catch (Exception e) {
+ System.out.println("β Error: " + e.getMessage());
+ }
+ }
+ }
+}
\ No newline at end of file