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

Update the system with a CVC3Generator class. 

Move all CVC3 code into CVC3Generator.  Currently it is just static methods,
next is to make implement an interface!

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

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

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

 */

public class BooleanVariableType implements VariableType {



    @Override

    public String getCVC3Definition(String variableName) {

        throw new UnsupportedOperationException("Not supported yet.");

    }

    

    @Override

    public boolean canCastToType(VariableType type) {

        return false;

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

+120 −4
Original line number Diff line number Diff line
@@ -4,20 +4,136 @@ 
 */

package ca.mcmaster.cas.matlab2smt;



import java.math.BigDecimal;

import java.math.BigInteger;

import org.apache.commons.lang3.StringUtils;



/**

 *

 * @author matthew

 */

public class CVC3Generator {

final public class CVC3Generator {



    private static String GetSignedFixedPointFunctionFor(MatlabOperation op) {

        switch (op) {

            case Addition:

                return "BVPLUS(";

            case Multiplication:

                return "BVMULT(";

            case GreaterThen:

                return "BVSGT(";

            case Equals:

                throw new IllegalArgumentException("Operation " + op + " doesn't have a signed fixed point function!");

        }

        throw new RuntimeException("Should never happen!");

    }



    private static String GetUnsignedFixedPointFunctionFor(MatlabOperation op) {

        switch (op) {

            case Addition:

                return "BVPLUS(";

            case Multiplication:

                return "BVMULT(";

            case GreaterThen:

                return "BVGT(";

            case Equals:

                throw new IllegalArgumentException("Operation " + op + " doesn't have a signed fixed point function!");

        }

        throw new RuntimeException("Should never happen!");

    }



    private static String GetInfixSymbolFor(MatlabOperation op) {

        switch (op) {

            case Addition:

                return "+";

            case Multiplication:

                return "*";

            case GreaterThen:

                return ">";

            case Equals:

                throw new IllegalArgumentException("Operation " + op + " doesn't have a signed fixed point function!");

        }

        throw new RuntimeException("Should never happen!");

    }



    public static String ConvertToOutputOp(MatlabOperation 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) {

                    FixedPointVariableType typeF = (FixedPointVariableType) type;

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

                } else {

                    return func;

                }

            case CenterOp:

                return GetInfixSymbolFor(op);

            default:

                throw new IllegalStateException("CVC3 Operation type asked for that doesn't exist!");

        }

    }



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

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

            return OperationType.Function;

        } else {

            return OperationType.CenterOp;

        }

    }



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

        switch (op.CVC3OpTypeForType(usedType)) {

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

            case CenterOp:

                return "(" + lhsExp + " " + op.convertToCVC3Op(usedType) + " " + rhsExp + ")";

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

            case Function:

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

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

            default:

                throw new IllegalStateException("Cannot output expression operation for requested operation type.");

        }

    }



    public static String GenerateVariableType(VariableType type) {

        if (type instanceof RealVariableType) {

            return "REAL";

        } else if (type instanceof FixedPointVariableType) {

            return "BITVECTOR(" + ((FixedPointVariableType) type).digits() + ")";

        } else if (type instanceof BooleanVariableType) {

            return "BOOLEAN";

        } else {

            throw new IllegalArgumentException("CVC3 Doesn't handle this variable type (Class: " + type.getClass().getName() + ")");

        }

    }



    public static String GenerateVariableDecleration(String name, VariableType type) {

        return name + ":" + CVC3Generator.GenerateVariableType(type) + ";";

    }



    public static String GenerateLiterlaValue(String value, VariableType requestedType) {

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

            return value;

        } else if (requestedType instanceof FixedPointVariableType) {

            FixedPointVariableType type = (FixedPointVariableType) requestedType;

            BigDecimal decimal = new BigDecimal(value);

            decimal = decimal.multiply(BigDecimal.valueOf(1 << type.fractionPart()));

            BigInteger intOut = decimal.toBigIntegerExact();



            //This gets the two's compliment representation.  Ugly for loop, but best I could find.

            String bits = "";

            for (int i = intOut.bitLength() - 1; i >= 0; --i) {

                System.out.println(intOut.testBit(i));

                bits += (intOut.testBit(i)) ? '1' : '0';

            }



            if (intOut.signum() < 0) {

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

            } else {

                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/FixedPointVariableType.java

+8 −13
Original line number Diff line number Diff line
@@ -28,11 +28,6 @@ final public class FixedPointVariableType implements VariableType { 
        return m_fractionPart;

    }



    @Override

    public String getCVC3Definition(String variableName) {

        return "BITVECTOR("+m_digits+")";

    }



    @Override

    public boolean canCastToType(VariableType type) {

        return false;
@@ -44,9 +39,9 @@ final public class FixedPointVariableType implements VariableType { 
            return false;

        } else {

            FixedPointVariableType other = (FixedPointVariableType) othero;

            if(other.m_isSigned == m_isSigned &&

                    other.m_digits == m_digits &&

                    other.m_fractionPart == m_fractionPart) {

            if (other.m_isSigned == m_isSigned

                    && other.m_digits == m_digits

                    && other.m_fractionPart == m_fractionPart) {

                return true;

            } else {

                return false;

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

+1 −1
Original line number Diff line number Diff line
@@ -11,5 +11,5 @@ package ca.mcmaster.cas.matlab2smt; 
public interface MatlabExpression {

    VariableType type();

    

    String getCVC3Output(VariableType requestedType);

    String getCheckerOutput(VariableType requestedType);

}

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

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

 */

final class MatlabExpressionOperation implements MatlabExpression, MatlabExpressionWithSubExpression {



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

        m_lhs = lhs;

        m_rhs = rhs;
@@ -40,12 +41,12 @@ final class MatlabExpressionOperation implements MatlabExpression, MatlabExpress 
    }



    @Override

    public String getCVC3Output(VariableType requestedType) {

    public String getCheckerOutput(VariableType requestedType) {

        VariableType usedType = type();

        assert usedType.equals(requestedType);



        String lhsExp = m_lhs.getCVC3Output(usedType);

        String rhsExp = m_rhs.getCVC3Output(usedType);

        String lhsExp = m_lhs.getCheckerOutput(usedType);

        String rhsExp = m_rhs.getCheckerOutput(usedType);



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

    }