Commit 510eb1e3 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Since expression outputs are now actually defined, make use of this fact. 

Since expression's outputs now generally work with their type correctly, make
use of this to try and ensure an expression is evaluated correctly.  Also
make sure that the requested type does match the type outputted, and test
that this occurs (for now, just in BinaryExpression and Variable).

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

@CVC_checker/CVC_checker.m

+1 −0
Original line number Diff line number Diff line
@@ -7,6 +7,7 @@ classdef CVC_checker 
        command = 'cvc3';

        data = [];

        generator = ca.mcmaster.cas.matlab2smt.CVC3Generator();

        boolean_type = ca.mcmaster.cas.matlab2smt.BooleanVariableType();

        

    end

@CVC_checker/matlab_to_cvc_syntax_translation.m

+1 −1
Original line number Diff line number Diff line
@@ -26,7 +26,7 @@ matlab_string = s; 


parser = ca.mcmaster.cas.matlab2smt.MatlabParser(var_def, matlab_string);

expr = parser.getRootExpression();

cvc_string = char(expr.getCheckerOutput(object.generator, expr.type()))

cvc_string = char(expr.getCheckerOutput(object.generator, object.boolean_type))



end

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

+3 −1
Original line number Diff line number Diff line
@@ -47,7 +47,9 @@ final class MatlabExpressionBinaryOperation implements MatlabExpression, MatlabE 
    @Override

    public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) {

        VariableType inputType = usedInputType();

        assert type().equals(requestedType);

        if (!type().equals(requestedType)) {

            throw new IllegalArgumentException("Requested output type is not the expression's output type!");

        }



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

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

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

+3 −1
Original line number Diff line number Diff line
@@ -28,7 +28,9 @@ public class Variable implements MatlabExpression, MatlabExpressionValue { 


    @Override

    public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) {

        assert m_type.equals(requestedType);

        if (!type().equals(requestedType)) {

            throw new IllegalArgumentException("Requested output type is not the expression's output type!");

        }

        return m_name;

    }

}

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

+11 −0
Original line number Diff line number Diff line
@@ -92,5 +92,16 @@ public class MatlabExpressionBinaryOperationTest { 
        assertEquals("(5 == 6)", exp.getCheckerOutput(generator, exp.type()));

    }



    /**

     * Test operations fails when a requested type is invalid!

     */

    @Test(expected=IllegalArgumentException.class)

    public void testInvalidOutputType() {

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

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



        exp.getCheckerOutput(generator, new RealVariableType()); //Returns a boolean, so will fail.

    }



    CheckerGenerator generator = new CVC3Generator();

}