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

Start adding support for the Boolean and operation. 

Start adding support for the boolean and operation.  Currently it works if
parsed correctly, but the next commit is necessary so it can be parsed.

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

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/CVC3Generator.java

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

            case Equals:

                return "=";

            case BooleanAnd:

                return "AND";

        }

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

    }

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/MatlabBinaryOperation.java

+13 −1
Original line number Diff line number Diff line
@@ -13,7 +13,9 @@ public enum MatlabBinaryOperation { 
    Addition,

    Multiplication,

    GreaterThen,

    Equals;

    Equals,



    BooleanAnd;



    static MatlabBinaryOperation getOpForSymbol(String text) {

        if (text.equals("+")) {
@@ -24,12 +26,22 @@ public enum MatlabBinaryOperation { 
            return GreaterThen;

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

            return Equals;

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

            return BooleanAnd;

        } else {

            throw new IllegalArgumentException("No such binary matlab operation defined (" + text + ")!");

        }

    }



    VariableType getOutputTypeForInput(VariableType inputType) {

        // Boolean inputs only work with a boolean input!

        if (this == BooleanAnd) {

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

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

            }

        }



        // Comparisions produce boolean outputs!

        switch(this) {

            case GreaterThen:

            case Equals:

Matlab2SMT/src/test/java/ca/mcmaster/cas/matlab2smt/MatlabExpressionBinaryOperationTest.java

+16 −0
Original line number Diff line number Diff line
@@ -103,5 +103,21 @@ public class MatlabExpressionBinaryOperationTest { 
        exp.getCheckerOutput(generator, new RealVariableType()); //Returns a boolean, so will fail.

    }



    /**

     * Test doing multiple boolean operations AND'd together.

     */

    @Test

    public void testBooleanAndFromComparision() {

        MatlabExpression l = new Variable("a", new RealVariableType()), r = new MatlabLiteral("6"),

                      l2 = new Variable("b", new RealVariableType()), r2 = new MatlabLiteral("8");

        MatlabExpressionBinaryOperation exp = new MatlabExpressionBinaryOperation(new MatlabExpressionBinaryOperation(l, MatlabBinaryOperation.Equals, r),

                MatlabBinaryOperation.BooleanAnd,

                new MatlabExpressionBinaryOperation(l2, MatlabBinaryOperation.Equals, r2));



        // Test when adding a Real var to a lit, type always becomes Real.

        assertEquals(new BooleanVariableType(), exp.type());

        assertEquals("((a = 6) AND (b = 8))", exp.getCheckerOutput(generator, exp.type()));

    }



    CheckerGenerator generator = new CVC3Generator();

}