Commit ce8e4bb5 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add support for the implication operator. 

Adds support for the implication operator in PVS (=>).  Matlab's support for
it is questionable, and thus ignored for now.  The operator is supported in
all layers, including generators.

Note that due to matlab not supporting all the operators, GenericGeneratorTest
now uses PVS to parse in its mega expression.  This changed the parsed's
expression's content, and thus the expression changed a little dramatically.

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

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/BinaryOperation.java

+3 −2
Original line number Diff line number Diff line
@@ -25,12 +25,13 @@ public enum BinaryOperation { 
    Equals,

    NotEquals,



    Implies,

    BooleanAnd,

    BooleanOr;



    Collection<VariableTypeMarker> getInputTypeForOutput(VariableTypeMarker outputType) {

        // Boolean inputs only work with a boolean input!

        if (this == BooleanAnd || this == BooleanOr || this == GreaterThen || this == GreaterThenEqual ||

        if (this == BooleanAnd || this == BooleanOr || this == Implies || this == GreaterThen || this == GreaterThenEqual ||

                this == LessThen || this == LessThenEqual || this == Equals || this == NotEquals) {

            if (!outputType.equals(new BooleanVariableType())) {

                throw new IllegalArgumentException("Boolean operators and comparisons require a boolean output type!");
@@ -52,7 +53,7 @@ public enum BinaryOperation { 


    public VariableType getOutputForInput(VariableType inputType) {

        // Boolean inputs only work with a boolean input!

        if (this == BooleanAnd || this == BooleanOr) {

        if (this == BooleanAnd || this == BooleanOr || this == Implies) {

            if (!inputType.equals(new BooleanVariableType())) {

                throw new IllegalArgumentException("Boolean operators require a boolean input type!");

            }

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/CVC3Generator.java

+2 −0
Original line number Diff line number Diff line
@@ -87,6 +87,8 @@ final public class CVC3Generator implements CheckerGenerator{ 
                return "AND";

            case BooleanOr:

                return "OR";

            case Implies:

                return "=>";

        }

        throw new RuntimeException("Should never happen!");

    }

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/SMTLIBGenerator.java

+2 −0
Original line number Diff line number Diff line
@@ -105,6 +105,8 @@ public class SMTLIBGenerator implements CheckerGenerator { 
                return "and";

            case BooleanOr:

                return "or";

            case Implies:

                return "=>";

        }

        throw new RuntimeException("Should never happen!  Asked for unhandled op: " + op + "!");

    }

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/PVSSimpleParser.g4

+20 −17
Original line number Diff line number Diff line
@@ -11,28 +11,30 @@ the extra pieces from it. It is also modified to make the associated pieces in 
// a precedence hierarchy for parsing expressions



// these are groups of operators that have equivalent precedences

g1: LOG_OR;

g2: LOG_AND;

g3: NEG;

g4: ( NEQ | EQ | GRTE | GRT | LSTE | LST );

g5: ( PLUS | MINUS );

g6: ( LEFTDIV | TIMES );

g7: MINUS;

g8: EXPONENTIATION;

g1: IMPLIES;

g2: LOG_OR;

g3: LOG_AND;

g4: NEG;

g5: ( NEQ | EQ | GRTE | GRT | LSTE | LST );

g6: ( PLUS | MINUS );

g7: ( LEFTDIV | TIMES );

g8: MINUS;

g9: EXPONENTIATION;



// the hierarchy is defined from LOWEST to HIGHEST priority.



expression : e0;



e0	: e1 g1 e0 | e1; // Logic OR

e1	: e2 g2 e1 | e2; // Logc AND

e2	: g3 e3 | e3; // Logc NOT

e3	: e3 g4 e4 | e4; // Comparison

e4	: e4 g5 e5 | e5; // Addition/Subtraction

e5	: e5 g6 e6 | e6; // Multiplication/Division

e6	: g7 e7 | e7; // Unary Minus

e7	: e7 g8 e8 | e8; // note: in PVS, exponentiation is left-associative

e8	: unary_expression;

e0	: e1 g1 e0 | e1; // Implies

e1	: e2 g2 e1 | e2; // Logic OR

e2	: e3 g3 e2 | e3; // Logc AND

e3	: g4 e4 | e4; // Logc NOT

e4	: e4 g5 e5 | e5; // Comparison

e5	: e5 g6 e6 | e6; // Addition/Subtraction

e6	: e6 g7 e7 | e7; // Multiplication/Division

e7	: g8 e8 | e8; // Unary Minus

e8	: e8 g9 e9 | e9; // note: in PVS, exponentiation is left-associative

e9	: unary_expression;



unary_expression

	: base_expression #BASE_EXPRESIION
@@ -55,6 +57,7 @@ id: i1=ID; 
// operators and assignments

//



IMPLIES : '=>';

LOG_OR	: 'OR';

LOG_AND	: 'AND';

LSTE	: '<=';

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/PVSSimpleParser.java

+22 −3
Original line number Diff line number Diff line
@@ -22,6 +22,7 @@ import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E5 
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E6Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E7Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E8Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E9Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G1Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G2Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G3Context;
@@ -30,6 +31,7 @@ import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G5 
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G6Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G7Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G8Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G9Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.IdContext;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.Literal_numberContext;

import org.antlr.v4.runtime.ANTLRInputStream;
@@ -156,6 +158,8 @@ final public class PVSSimpleParser { 
                return BinaryOperation.Equals;

            } else if (text.equals("/=")) {

                return BinaryOperation.NotEquals;

            } else if (text.equals("=>")) {

                return BinaryOperation.Implies;

            } else if (text.equals("AND")) {

                return BinaryOperation.BooleanAnd;

            } else if (text.equals("OR")) {
@@ -221,6 +225,11 @@ final public class PVSSimpleParser { 
            incrementLevel();

        }



        @Override

        public void enterE9(E9Context ctx) {

            incrementLevel();

        }



        @Override

        public void exitE0(E0Context ctx) {

            decrementLevel();
@@ -266,6 +275,11 @@ final public class PVSSimpleParser { 
            decrementLevel();

        }



        @Override

        public void exitE9(E9Context ctx) {

            decrementLevel();

        }



        @Override

        public void enterG1(G1Context ctx) {

            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));
@@ -278,12 +292,12 @@ final public class PVSSimpleParser { 


        @Override

        public void enterG3(G3Context ctx) {

            addPrefixUnaryOperation(new ExpressionUnaryOperation(UnaryOperation.Negation, null)); // This is always negation.

            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));

        }



        @Override

        public void enterG4(G4Context ctx) {

            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));

            addPrefixUnaryOperation(new ExpressionUnaryOperation(UnaryOperation.Negation, null)); // This is always negation.

        }



        @Override
@@ -298,11 +312,16 @@ final public class PVSSimpleParser { 


        @Override

        public void enterG7(G7Context ctx) {

            addPrefixUnaryOperation(new ExpressionUnaryOperation(UnaryOperation.Minus, null)); // This is always minus.

            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));

        }



        @Override

        public void enterG8(G8Context ctx) {

            addPrefixUnaryOperation(new ExpressionUnaryOperation(UnaryOperation.Minus, null)); // This is always minus.

        }



        @Override

        public void enterG9(G9Context ctx) {

            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));

        }