Commit 6d4d9cee authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Use proper grammar for SMTLIB output. 

To handle the case when more complicated output is received from SMTLIB,
properly parse SMTLIB output.

Due to ANTLR trying to consume the full stream, the SMTLIB response is first
put in a string.  A simple algorithm, using the brackets, is used to find the
beginning and end.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10722 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 62d14239

Matlab2SMT/src/main/java/ca/mcmaster/cas/smtlibchecker/CheckerRunner.java

+46 −42
Original line number Diff line number Diff line
@@ -21,7 +21,11 @@ import ca.mcmaster.cas.matlab2smt.Variable; 
import ca.mcmaster.cas.matlab2smt.VariableParser;

import ca.mcmaster.cas.tablularexpression.HierarchcialGridCheckerWalkerGenerator;

import ca.mcmaster.cas.tablularexpression.HierarchicalGrid;

import org.apache.commons.lang3.StringUtils;

import org.antlr.v4.runtime.ANTLRInputStream;

import org.antlr.v4.runtime.CommonTokenStream;

import org.antlr.v4.runtime.misc.NotNull;

import org.antlr.v4.runtime.tree.ParseTree;

import org.antlr.v4.runtime.tree.ParseTreeWalker;



import java.io.BufferedReader;

import java.io.IOException;
@@ -126,46 +130,30 @@ final public class CheckerRunner { 
        if(reader.markSupported() == false) {

            throw new IllegalArgumentException("Reader must support marks!");

        }

        Map<String, String> ret = new HashMap<String, String>();

        final Map<String, String> ret = new HashMap<String, String>();



        boolean done = false;

        StringBuilder varname = new StringBuilder(), varvalue = new StringBuilder();

        StringBuilder input = new StringBuilder();



        char nextChar = consumeWhitespaceAndReturnNextChar(reader);

        if(nextChar != '(') {

            throw new IllegalArgumentException("Bad input, want (, got " + nextChar + "!");

        int bracketMismatch = 1; // This starts with a (, so we immediately have a a mismatch.

        char nextChar = getNextChar(reader);

        if (nextChar != '(') { // Should start with a ( for output.

            throw new IllegalStateException("Bad input, wanted a ( to start, got " + nextChar);

        }



        nextChar = consumeWhitespaceAndReturnNextChar(reader);

        while(nextChar == '(') {

            varname.setLength(0);

            varvalue.setLength(0);



            nextChar = consumeWhitespaceAndReturnNextChar(reader);

            varname.append(nextChar);

            nextChar = getNextChar(reader);

            while(!isWhitespace(nextChar)) {

                varname.append(nextChar);

                nextChar = getNextChar(reader);

            }



            nextChar = consumeWhitespaceAndReturnNextChar(reader);

            varvalue.append(nextChar);

            nextChar = getNextChar(reader);

            while(!isWhitespace(nextChar) && nextChar != ')') {

                varvalue.append(nextChar);

        input.append(nextChar);

        while(bracketMismatch != 0) {

            nextChar = getNextChar(reader);

            switch (nextChar) {

                case '(':

                    bracketMismatch++;

                    break;

                case ')':

                    bracketMismatch--;

                    break;

            }



            ret.put(varname.toString(), varvalue.toString());



            nextChar = consumeWhitespaceAndReturnNextChar(reader);

        }



        if(nextChar != ')') {

            throw new IllegalArgumentException("Bad input, want (, got " + nextChar + "!");

            input.append(nextChar);

        }



        // Finally, clear the new line, so the output is now clear.

        do {

            reader.mark(5);

            nextChar = getNextChar(reader);
@@ -173,7 +161,31 @@ final public class CheckerRunner { 
        if(!isWhitespace(nextChar)) {

            reader.reset();

        }

        System.out.println(input);



        ANTLRInputStream antlrInput = new ANTLRInputStream(input.toString());

        System.out.println(input);



        // create a lexer that feeds off of input CharStream

        SMTLibOutParserLexer lexer = new SMTLibOutParserLexer(antlrInput);



        // create a buffer of tokens pulled from the lexer

        CommonTokenStream tokens = new CommonTokenStream(lexer);



        // create a parser that feeds off the tokens buffer

        SMTLibOutParserParser parser = new SMTLibOutParserParser(tokens);



        ParseTree tree = parser.valuelist();

        ParseTreeWalker walker = new ParseTreeWalker();

        SMTLibOutParserListener listener = new SMTLibOutParserBaseListener() {

            @Override

            public void enterValue(@NotNull SMTLibOutParserParser.ValueContext ctx) {

                System.out.println(ctx.ID().getText());

                System.out.println(ctx.RATIONAL().getText());

                ret.put(ctx.ID().getText(), ctx.RATIONAL().getText());

            }

        };

        walker.walk(listener, tree);

        return ret;

    }
@@ -192,12 +204,4 @@ final public class CheckerRunner { 
        }

        return false;

    }



    private static char consumeWhitespaceAndReturnNextChar(Reader reader) throws IOException {

        char c = getNextChar(reader);

        while(isWhitespace(c)) {

            c = getNextChar(reader);

        }

        return c;

    }

}

Matlab2SMT/src/main/java/ca/mcmaster/cas/smtlibchecker/SMTLibOutParser.g4

0 → 100644
+8 −0
Original line number Diff line number Diff line 
grammar SMTLibOutParser;



valuelist: '(' value+ ')'; //Build list of variables

value:     '(' ID RATIONAL ')';



ID: [a-zA-Z][a-zA-Z0-9]*; //Variable identifier.  Start with letter, then alpha numerical allowed.

RATIONAL: [0-9]+(.[0-9]+)?;

WS : [ \t\r\n]+ -> skip ; // skip spaces, tabs, newlines