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

Prepare for the new unary operation support with some renames. 

Various classes/functions (ex MatlabOperation) are not preapred to deal with
unary operations, and realistically probably never will.  Thus just rename
to include binary in the name (ex MatlabBinaryOperation).  Also push the
changes down so everything still works.

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

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

+8 −8
Original line number Diff line number Diff line
@@ -14,7 +14,7 @@ import org.apache.commons.lang3.StringUtils; 
 */

final public class CVC3Generator implements CheckerGenerator{



    private static String GetSignedFixedPointFunctionFor(MatlabOperation op) {

    private static String GetSignedFixedPointFunctionFor(MatlabBinaryOperation op) {

        switch (op) {

            case Addition:

                return "BVPLUS(";
@@ -28,7 +28,7 @@ final public class CVC3Generator implements CheckerGenerator{ 
        throw new RuntimeException("Should never happen!");

    }



    private static String GetUnsignedFixedPointFunctionFor(MatlabOperation op) {

    private static String GetUnsignedFixedPointFunctionFor(MatlabBinaryOperation op) {

        switch (op) {

            case Addition:

                return "BVPLUS(";
@@ -42,7 +42,7 @@ final public class CVC3Generator implements CheckerGenerator{ 
        throw new RuntimeException("Should never happen!");

    }



    private static String GetInfixSymbolFor(MatlabOperation op) {

    private static String GetInfixSymbolFor(MatlabBinaryOperation op) {

        switch (op) {

            case Addition:

                return "+";
@@ -56,14 +56,14 @@ final public class CVC3Generator implements CheckerGenerator{ 
        throw new RuntimeException("Should never happen!");

    }



    protected static String ConvertToOutputOp(MatlabOperation op, VariableType type) {

    protected static String ConvertToOutputOp(MatlabBinaryOperation op, VariableType type) {

        switch (OpTypeForVariableType(op, type)) {

            case Function:

                String func = GetSignedFixedPointFunctionFor(op);

                if (!((FixedPointVariableType) type).isSigned()) {

                    func = GetUnsignedFixedPointFunctionFor(op);

                }

                if ((op == MatlabOperation.Addition || op == MatlabOperation.Multiplication) && type instanceof FixedPointVariableType) {

                if ((op == MatlabBinaryOperation.Addition || op == MatlabBinaryOperation.Multiplication) && type instanceof FixedPointVariableType) {

                    FixedPointVariableType typeF = (FixedPointVariableType) type;

                    return func + typeF.digits() + ",";

                } else {
@@ -76,8 +76,8 @@ final public class CVC3Generator implements CheckerGenerator{ 
        }

    }



    private static OperationType OpTypeForVariableType(MatlabOperation op, VariableType type) {

        if (type instanceof FixedPointVariableType && op != MatlabOperation.Equals) {

    private static OperationType OpTypeForVariableType(MatlabBinaryOperation op, VariableType type) {

        if (type instanceof FixedPointVariableType && op != MatlabBinaryOperation.Equals) {

            return OperationType.Function;

        } else {

            return OperationType.CenterOp;
@@ -85,7 +85,7 @@ final public class CVC3Generator implements CheckerGenerator{ 
    }



    @Override

    public String GenerateOperation(MatlabOperation op, String lhsExp, String rhsExp, VariableType usedType) {

    public String GenerateBinaryOperation(MatlabBinaryOperation op, String lhsExp, String rhsExp, VariableType usedType) {

        switch (CVC3Generator.OpTypeForVariableType(op, usedType)) {

            case CenterOp:

                return "(" + lhsExp + " " + CVC3Generator.ConvertToOutputOp(op, usedType) + " " + rhsExp + ")";

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

+1 −1
Original line number Diff line number Diff line
@@ -9,7 +9,7 @@ package ca.mcmaster.cas.matlab2smt; 
 * @author matthew

 */

public interface CheckerGenerator {

    public String GenerateOperation(MatlabOperation op, String lhsExp, String rhsExp, VariableType usedType);

    public String GenerateBinaryOperation(MatlabBinaryOperation op, String lhsExp, String rhsExp, VariableType usedType);

    public String GenerateLiterlaValue(String value, VariableType requestedType);

    public String GenerateVariableDecleration(Variable var);

    public String GenerateVariableType(VariableType type);

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

+3 −3
Original line number Diff line number Diff line
@@ -8,14 +8,14 @@ package ca.mcmaster.cas.matlab2smt; 
 *

 * @author matthew

 */

public enum MatlabOperation {

public enum MatlabBinaryOperation {



    Addition,

    Multiplication,

    GreaterThen,

    Equals;



    static MatlabOperation getOpForSymbol(String text) {

    static MatlabBinaryOperation getOpForSymbol(String text) {

        if (text.equals("+")) {

            return Addition;

        } else if (text.equals("*")) {
@@ -25,7 +25,7 @@ public enum MatlabOperation { 
        } else if (text.equals("==")) {

            return Equals;

        } else {

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

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

        }

    }

}

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

+4 −4
Original line number Diff line number Diff line
@@ -8,9 +8,9 @@ package ca.mcmaster.cas.matlab2smt; 
 *

 * @author matthew

 */

final class MatlabExpressionOperation implements MatlabExpression, MatlabExpressionWithSubExpression {

final class MatlabExpressionBinaryOperation implements MatlabExpression, MatlabExpressionWithSubExpression {



    MatlabExpressionOperation(MatlabExpression lhs, MatlabOperation op, MatlabExpression rhs) {

    MatlabExpressionBinaryOperation(MatlabExpression lhs, MatlabBinaryOperation op, MatlabExpression rhs) {

        m_lhs = lhs;

        m_rhs = rhs;

        m_op = op;
@@ -48,7 +48,7 @@ final class MatlabExpressionOperation implements MatlabExpression, MatlabExpress 
        String lhsExp = m_lhs.getCheckerOutput(generator, usedType);

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



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

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

    }



    @Override
@@ -62,5 +62,5 @@ final class MatlabExpressionOperation implements MatlabExpression, MatlabExpress 
    }



    MatlabExpression m_lhs, m_rhs;

    MatlabOperation m_op;

    MatlabBinaryOperation m_op;

}

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

+5 −5
Original line number Diff line number Diff line
@@ -80,7 +80,7 @@ final public class MatlabParser implements MatlabExpressionWithSubExpression { 
        m_opStack.peekFirst().op.setSubExpression(expressionValue);

    }



    private void addExpressionOperation(MatlabExpressionOperation op) {

    private void addExpressionBinaryOperation(MatlabExpressionBinaryOperation op) {

        System.out.println("" + m_level + " " + m_opStack.peekFirst().level);

        if (m_rootExpression == null) {

            throw new IllegalStateException("It should not be possible to have"
@@ -255,22 +255,22 @@ final public class MatlabParser implements MatlabExpressionWithSubExpression { 


        @Override

        public void enterG1(G1Context ctx) {

            addExpressionOperation(new MatlabExpressionOperation(null, MatlabOperation.getOpForSymbol(ctx.getText()), null));

            addExpressionBinaryOperation(new MatlabExpressionBinaryOperation(null, MatlabBinaryOperation.getOpForSymbol(ctx.getText()), null));

        }



        @Override

        public void enterG2(G2Context ctx) {

            addExpressionOperation(new MatlabExpressionOperation(null, MatlabOperation.getOpForSymbol(ctx.getText()), null));

            addExpressionBinaryOperation(new MatlabExpressionBinaryOperation(null, MatlabBinaryOperation.getOpForSymbol(ctx.getText()), null));

        }



        @Override

        public void enterG3(G3Context ctx) {

            addExpressionOperation(new MatlabExpressionOperation(null, MatlabOperation.getOpForSymbol(ctx.getText()), null));

            addExpressionBinaryOperation(new MatlabExpressionBinaryOperation(null, MatlabBinaryOperation.getOpForSymbol(ctx.getText()), null));

        }



        @Override

        public void enterG4(G4Context ctx) {

            addExpressionOperation(new MatlabExpressionOperation(null, MatlabOperation.getOpForSymbol(ctx.getText()), null));

            addExpressionBinaryOperation(new MatlabExpressionBinaryOperation(null, MatlabBinaryOperation.getOpForSymbol(ctx.getText()), null));

        }



        @Override