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

Add the necessary pieces to request the right type out of a binary expression. 

Since binary expressions can actually change the type (for instance, comparisions
switch the type for the number input to boolean), handle this so calls further
up the chain don't break (for instance, boolean operators, ex AND).

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

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

+9 −0
Original line number Diff line number Diff line
@@ -28,4 +28,13 @@ public enum MatlabBinaryOperation { 
            throw new IllegalArgumentException("No such binary matlab operation defined (" + text + ")!");

        }

    }



    VariableType getOutputTypeForInput(VariableType inputType) {

        switch(this) {

            case GreaterThen:

            case Equals:

                return new BooleanVariableType();

        }

        return inputType;

    }

}

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

+11 −7
Original line number Diff line number Diff line
@@ -24,8 +24,7 @@ final class MatlabExpressionBinaryOperation implements MatlabExpression, MatlabE 
        m_rhs = expr;

    }



    @Override

    public VariableType type() {

    private VariableType usedInputType() {

        VariableType lhs_type = m_lhs.type();

        VariableType rhs_type = m_rhs.type();
@@ -40,15 +39,20 @@ final class MatlabExpressionBinaryOperation implements MatlabExpression, MatlabE 
        }

    }



    @Override

    public VariableType type() {

        return m_op.getOutputTypeForInput(usedInputType());

    }



    @Override

    public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) {

        VariableType usedType = type();

        assert usedType.equals(requestedType);

        VariableType inputType = usedInputType();

        assert type().equals(requestedType);



        String lhsExp = m_lhs.getCheckerOutput(generator, usedType);

        String rhsExp = m_rhs.getCheckerOutput(generator, usedType);

        String lhsExp = m_lhs.getCheckerOutput(generator, inputType);

        String rhsExp = m_rhs.getCheckerOutput(generator, inputType);



        return generator.GenerateBinaryOperation(m_op, lhsExp, rhsExp, usedType);

        return generator.GenerateBinaryOperation(m_op, lhsExp, rhsExp, inputType);

    }



    @Override

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

+19 −2
Original line number Diff line number Diff line
@@ -71,8 +71,25 @@ public class MatlabExpressionBinaryOperationTest { 
        Variable var = new Variable("A", new RealVariableType());

        

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

        assertEquals(new RealVariableType(), new MatlabExpressionBinaryOperation(lit, MatlabBinaryOperation.Equals, var).type());

        assertEquals(new RealVariableType(), new MatlabExpressionBinaryOperation(var, MatlabBinaryOperation.Equals, lit).type());

        assertEquals(new RealVariableType(), new MatlabExpressionBinaryOperation(lit, MatlabBinaryOperation.Addition, var).type());

        assertEquals(new RealVariableType(), new MatlabExpressionBinaryOperation(var, MatlabBinaryOperation.Addition, lit).type());



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

        assertEquals(new BooleanVariableType(), new MatlabExpressionBinaryOperation(lit, MatlabBinaryOperation.Equals, var).type());

        assertEquals(new BooleanVariableType(), new MatlabExpressionBinaryOperation(var, MatlabBinaryOperation.Equals, lit).type());

    }



    /**

     * Test operations changing types (== doing REAL+REAL -> BOOLEAN)

     */

    @Test

    public void testCastingOperations() {

        MatlabLiteral l = new MatlabLiteral("5"), r = new MatlabLiteral("6");

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



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

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

        assertEquals("(5 == 6)", exp.getCheckerOutput(generator, exp.type()));

    }



    CheckerGenerator generator = new CVC3Generator();

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

+2 −1
Original line number Diff line number Diff line
@@ -4,6 +4,7 @@ 
 */

package ca.mcmaster.cas.matlab2smt.test;



import ca.mcmaster.cas.matlab2smt.BooleanVariableType;

import ca.mcmaster.cas.matlab2smt.CVC3Generator;

import ca.mcmaster.cas.matlab2smt.CheckerGenerator;

import ca.mcmaster.cas.matlab2smt.MatlabExpression;
@@ -118,7 +119,7 @@ public class MatlabParserTest { 
        MatlabParser parser = new MatlabParser(null, "5 > 5\n");

        MatlabExpression expr = parser.getRootExpression();

        

        assertEquals(new MatlabLiteral(null).type(), expr.type());

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

        assertEquals("(5 > 5)", expr.getCheckerOutput(generator, expr.type()));

    }

    CheckerGenerator generator = new CVC3Generator();