Commit 6448830d authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Massive change for type handling in expressions. 

When dealing with expressions, and generating output for them, types have
to be exactly known.  However, when two literals are added together (like:
5+5), the type to use for that is unknown.  To fix this issue, type information
has to be forced down the pipe.  So know the addition operation now knows it
needs to produce a particular type (ex Real or Fixed Point), and then tests
what the subexpressions can produce (for literals, they can produce either,
but a variable can only be what it is).

For Real, that is fine.  However a fixed point can take an infinite number of
different possibilities, and one cannot test for every combination.  So instead
a type "marker" is introduced.  This marker instead identifies that a fixed
point type is generally wanted, but specifics are unknown.  The system will
query for an appropriate type, and requires the specific type is returned, and
not a marker.  All types are also markers for themselves, so Reals, for instance,
don't need anything special.

While the marker system sounds good in theory, it currently is fully implemented,
so fixed point is currently broken.

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

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

+1 −1
Original line number Diff line number Diff line
@@ -125,7 +125,7 @@ final public class CVC3Generator implements CheckerGenerator{ 


    @Override

    public String GenerateLiterlaValue(String value, VariableType requestedType) {

        if (requestedType instanceof RealVariableType || requestedType instanceof MatlabLiteral.LiteralNumberType) {

        if (requestedType instanceof RealVariableType) {

            return value;

        } else if (requestedType instanceof FixedPointVariableType) {

            FixedPointVariableType type = (FixedPointVariableType) requestedType;

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

+2 −0
Original line number Diff line number Diff line
@@ -61,4 +61,6 @@ final public class FixedPointVariableType implements VariableType { 
    private final int m_fractionPart;

    private final int m_digits;

    private final boolean m_isSigned;



    public static class Marker implements VariableTypeMarker {}

}

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

+29 −2
Original line number Diff line number Diff line
@@ -4,6 +4,9 @@ 
 */

package ca.mcmaster.cas.matlab2smt;



import java.util.Arrays;

import java.util.Collection;



/**

 *

 * @author matthew
@@ -52,9 +55,30 @@ public enum MatlabBinaryOperation { 
        }

    }



    VariableType getOutputTypeForInput(VariableType inputType) {

    Collection<VariableTypeMarker> getInputTypeForOutput(VariableTypeMarker outputType) {

        // Boolean inputs only work with a boolean input!

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

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

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

                throw new IllegalArgumentException("Boolean operators and comparisons require a boolean output type!");

            }

        }



        // Comparisions produce boolean outputs!

        switch(this) {

            case GreaterThen:

            case GreaterThenEqual:

            case LessThen:

            case LessThenEqual:

            case Equals:

                return Arrays.asList(new VariableTypeMarker[]{new RealVariableType(), new FixedPointVariableType.Marker()});

        }

        return Arrays.asList(new VariableTypeMarker[]{outputType});

    }



    public VariableType getOutputForInput(VariableType inputType) {

        // Boolean inputs only work with a boolean input!

        if (this == BooleanAnd) {

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

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

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

            }
@@ -63,6 +87,9 @@ public enum MatlabBinaryOperation { 
        // Comparisions produce boolean outputs!

        switch(this) {

            case GreaterThen:

            case GreaterThenEqual:

            case LessThen:

            case LessThenEqual:

            case Equals:

                return new BooleanVariableType();

        }

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

+4 −1
Original line number Diff line number Diff line
@@ -10,7 +10,10 @@ package ca.mcmaster.cas.matlab2smt; 
 */

public interface MatlabExpression {



    VariableType type();

    /* This methods returns an actual variable type for the requested input type.  If due to the setup of the system,

    *  this is not possible, then this function should return null.

    */

    VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType);



    String getCheckerOutput(CheckerGenerator generator, VariableType requestedType);

}

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

+26 −18
Original line number Diff line number Diff line
@@ -4,6 +4,8 @@ 
 */

package ca.mcmaster.cas.matlab2smt;



import java.util.Collection;



/**

 *

 * @author matthew
@@ -24,37 +26,43 @@ final class MatlabExpressionBinaryOperation implements MatlabExpression, MatlabE 
        m_rhs = expr;

    }



    private VariableType usedInputType() {

        VariableType lhs_type = m_lhs.type();

        VariableType rhs_type = m_rhs.type();



        if (lhs_type.equals(rhs_type)) {

            return lhs_type;

        } else if (lhs_type.canCastToType(rhs_type)) {

            return rhs_type;

        } else if (rhs_type.canCastToType(lhs_type)) {

            return lhs_type;

        } else {

            throw new IllegalStateException("Incompatible types are used together!");

    private VariableType getInputTypeForOutput(VariableTypeMarker requestedType) {

        Collection<VariableTypeMarker> allowedInputTypes = m_op.getInputTypeForOutput(requestedType);

        for(VariableTypeMarker allowedType : allowedInputTypes) {

            VariableType inputType = m_lhs.actualOutputTypeForRequestedOutput(allowedType);

            if(inputType != null &&

                    m_rhs.actualOutputTypeForRequestedOutput(inputType) != null) {

                return inputType;

            }

            inputType = m_rhs.actualOutputTypeForRequestedOutput(allowedType);

            if(inputType != null &&

                    m_lhs.actualOutputTypeForRequestedOutput(inputType) != null) {

                return inputType;

            }

        }

        return null;

    }



    @Override

    public VariableType type() {

        return m_op.getOutputTypeForInput(usedInputType());

    public VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType) {

        VariableType inputType = getInputTypeForOutput(requestedType);

        if (inputType != null) {

            return m_op.getOutputForInput(inputType);

        }

        return null;

    }



    @Override

    public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) {

        VariableType inputType = usedInputType();

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

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

        VariableType inputType = getInputTypeForOutput(requestedType);

        if (inputType == null) {

            throw new IllegalArgumentException("Requested output type is not valid for the expression's output type (" + requestedType.getClass().getSimpleName() + "!");

        }



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

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



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

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

    }



    @Override