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

Fix some bugs, and allow unsigned integers. 


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

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

+2 −2
Original line number Diff line number Diff line
@@ -41,9 +41,9 @@ public final class MatlabLiteral implements MatlabExpression, MatlabExpressionVa 
            }

            

            if(intOut.signum() < 0) {

                return "0bit" + StringUtils.repeat('1', type.digits() - bits.length()) + bits;

                return "0bin" + StringUtils.repeat('1', type.digits() - bits.length()) + bits;

            } else {

                return "0bit" + StringUtils.repeat('0', type.digits() - bits.length()) + bits;

                return "0bin" + StringUtils.repeat('0', type.digits() - bits.length()) + bits;

            }

        } else {

            throw new IllegalArgumentException("Can't cast literal to that type!");

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

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

 */

enum MatlabOperation {

    Addition("+", "BVPLUS("),

    GreaterThen(">", "BVSGT("),

    Equals("=", "=");

    Addition("+", "BVPLUS(", "BVPLUS("),

    GreaterThen(">", "BVSGT(", "BVGT("),

    Equals("=", "=", "=");



    static MatlabOperation getOpForSymbol(String text) {

        if(text.equals("+")) {
@@ -25,19 +25,24 @@ enum MatlabOperation { 
        }

    }



    MatlabOperation(String CVC3VersionCenter, String CVC3VersionFunction){

    MatlabOperation(String CVC3VersionCenter, String CVC3VersionFunctionSigned, String CVC3VersionFunctionUnsigned){

        m_CVC3VersionCenter = CVC3VersionCenter;

        m_CVC3VersionFunction = CVC3VersionFunction;

        m_CVC3VersionFunctionSigned = CVC3VersionFunctionSigned;

        m_CVC3VersionFunctionUnsigned = CVC3VersionFunctionUnsigned;

    }

    

    String convertToCVC3Op(VariableType type){

        switch(CVC3OpTypeForType(type)) {

            case Function:

                String func = m_CVC3VersionFunctionSigned;

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

                    func = m_CVC3VersionFunctionUnsigned;

                }

                if(this == Addition && type instanceof FixedPointVariableType) {

                    FixedPointVariableType typeF = (FixedPointVariableType)type;

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

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

                } else {

                    return m_CVC3VersionFunction;

                    return func;

                }

            case CenterOp:

                return m_CVC3VersionCenter;
@@ -48,14 +53,11 @@ enum MatlabOperation { 
    

    OperationType CVC3OpTypeForType(VariableType type) {

        if(type instanceof FixedPointVariableType && this != Equals) {

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

                throw new UnsupportedOperationException("Don't support unsigned operations yet!");

            }

            return OperationType.Function;

        } else {

            return OperationType.CenterOp;

        }

    }

    

    String m_CVC3VersionCenter, m_CVC3VersionFunction;

    String m_CVC3VersionCenter, m_CVC3VersionFunctionSigned, m_CVC3VersionFunctionUnsigned;

}

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

+6 −6
Original line number Diff line number Diff line
@@ -50,8 +50,8 @@ public class MatlabLiteralTest { 
    public void testGetCVC3Output() {

        MatlabLiteral instance = new MatlabLiteral("5");

        assertEquals("5", instance.getCVC3Output(new RealVariableType()));

        assertEquals("0bit00101", instance.getCVC3Output(new FixedPointVariableType(true, 5, 0)));

        assertEquals("0bit01010", instance.getCVC3Output(new FixedPointVariableType(true, 5, 1)));

        assertEquals("0bin00101", instance.getCVC3Output(new FixedPointVariableType(true, 5, 0)));

        assertEquals("0bin01010", instance.getCVC3Output(new FixedPointVariableType(true, 5, 1)));

    }



    /**
@@ -60,15 +60,15 @@ public class MatlabLiteralTest { 
    @Test

    public void testCVC3OutputOnInterestingFixedPoint() {

        MatlabLiteral instance = new MatlabLiteral("0");

        assertEquals("0bit00000", instance.getCVC3Output(new FixedPointVariableType(true, 5, 1)));

        assertEquals("0bin00000", instance.getCVC3Output(new FixedPointVariableType(true, 5, 1)));

        

        instance = new MatlabLiteral("5.5");

        assertEquals("0bit01011", instance.getCVC3Output(new FixedPointVariableType(true, 5, 1)));

        assertEquals("0bin01011", instance.getCVC3Output(new FixedPointVariableType(true, 5, 1)));

        

        instance = new MatlabLiteral("-5.5");

        assertEquals("0bit10101", instance.getCVC3Output(new FixedPointVariableType(true, 5, 1)));

        assertEquals("0bin10101", instance.getCVC3Output(new FixedPointVariableType(true, 5, 1)));

        

        instance = new MatlabLiteral("-5");

        assertEquals("0bit11011", instance.getCVC3Output(new FixedPointVariableType(true, 5, 0)));

        assertEquals("0bin11011", instance.getCVC3Output(new FixedPointVariableType(true, 5, 0)));

    }

}