Commit 32c57bec authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Handle negative and fractional outputs from SMTLIB. 

Handle the negative and fractional outputs from SMTLIB.  This required
extending the SMTLIB output grammar to accept negative and division operations.
Currently the support is cheated some, so that only the necessary pieces are
actually parsed.  Further support for more operations will require extending
the support further.

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

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

+30 −5
Original line number Diff line number Diff line
@@ -161,10 +161,8 @@ 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);
@@ -180,10 +178,37 @@ final public class CheckerRunner { 
        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());

                id = ctx.ID().getText();

                value = "";

            }



            @Override

            public void enterNegative(@NotNull SMTLibOutParserParser.NegativeContext ctx) {

                value = "(- ";

            }



            @Override

            public void exitSingle(@NotNull SMTLibOutParserParser.SingleContext ctx) {

                value += ctx.getText();

            }



            @Override

            public void exitFraction(@NotNull SMTLibOutParserParser.FractionContext ctx) {

                value += "(" + ctx.RATIONAL(0).getText() + " / " + ctx.RATIONAL(1).getText() + ")";

            }



            @Override

            public void exitNegative(@NotNull SMTLibOutParserParser.NegativeContext ctx) {

                value += ')';

            }



            @Override

            public void exitExpr(@NotNull SMTLibOutParserParser.ExprContext ctx) {

                ret.put(id, value);

            }



            String id = "";

            String value;

        };

        walker.walk(listener, tree);

        return ret;

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

+10 −1
Original line number Diff line number Diff line 
grammar SMTLibOutParser;



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

value:     '(' ID RATIONAL ')';

value:     '(' ID expr ')';



expr: single |

      fraction |

      negative;



negative: '(-' fraction ')' |

          '(-' single ')';

single: RATIONAL;

fraction: '(/' RATIONAL RATIONAL ')';



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

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

Matlab2SMT/src/test/java/ca/mcmaster/cas/smtlibchecker/CheckerRunnerTest.java

+53 −0
Original line number Diff line number Diff line
@@ -59,4 +59,57 @@ public class CheckerRunnerTest { 
        assertEquals("0.0", res.get(1).SampleValues.get("x"));

        assertEquals("0.0", res.get(1).SampleValues.get("z"));

    }

    @Test

    public void TestRunningZ3WithNegative() {

        HierarchicalGrid grid = new HierarchicalGrid();

        List<HierarchicalCell> topCells = grid.getSubHiearchy();



        topCells.add(new HierarchicalCell("x > 0"));

        topCells.add(new HierarchicalCell("x == 0"));

        topCells.add(new HierarchicalCell("0 > x"));



        List<HierarchicalCell> nextGrid = topCells.get(1).getSubHiearchy();

        nextGrid.add(new HierarchicalCell("z > 0"));

        nextGrid.add(new HierarchicalCell("z == 0"));

        nextGrid.add(new HierarchicalCell("z == -1"));

        nextGrid.add(new HierarchicalCell("0 > z"));



        //nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0"));



        List<CheckerRunnerResult> res = CheckerRunner.RunZ3(grid, new VariableParser("x,z"));

        assertEquals(1, res.size());

        assertEquals(2, res.get(0).SampleValues.size());

        assertEquals("0.0", res.get(0).SampleValues.get("x"));

        assertEquals("(- 1.0)", res.get(0).SampleValues.get("z"));

    }

    @Test

    public void TestRunningZ3WithFractionalReturn() {

        HierarchicalGrid grid = new HierarchicalGrid();

        List<HierarchicalCell> topCells = grid.getSubHiearchy();



        topCells.add(new HierarchicalCell("x > 0"));

        topCells.add(new HierarchicalCell("x == 0"));

        topCells.add(new HierarchicalCell("x == 2.5"));

        topCells.add(new HierarchicalCell("0 > x"));



        List<CheckerRunnerResult> res = CheckerRunner.RunZ3(grid, new VariableParser("x"));

        assertEquals(1, res.size());

        assertEquals(1, res.get(0).SampleValues.size());

        assertEquals("(5.0 / 2.0)", res.get(0).SampleValues.get("x"));

    }

    @Test

    public void TestRunningZ3WithNegativeFractionalReturn() {

        HierarchicalGrid grid = new HierarchicalGrid();

        List<HierarchicalCell> topCells = grid.getSubHiearchy();



        topCells.add(new HierarchicalCell("x > 0"));

        topCells.add(new HierarchicalCell("x == 0"));

        topCells.add(new HierarchicalCell("x == -2.5"));

        topCells.add(new HierarchicalCell("0 > x"));



        List<CheckerRunnerResult> res = CheckerRunner.RunZ3(grid, new VariableParser("x"));

        assertEquals(1, res.size());

        assertEquals(1, res.get(0).SampleValues.size());

        assertEquals("(- (5.0 / 2.0))", res.get(0).SampleValues.get("x"));

    }

}