Commit 0856ff05 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Have CVC3 output handle types. 


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

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();

    String getCVC3Output(VariableType requestedType);

}

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

+4 −2
Original line number Diff line number Diff line
@@ -40,8 +40,10 @@ final class MatlabExpressionOperation implements MatlabExpression { 
    }



    @Override

    public String getCVC3Output() {

        return "(" + m_lhs.getCVC3Output() + " " + m_op.convertToCVC3Op() + " " + m_rhs.getCVC3Output() + ")";

    public String getCVC3Output(VariableType requestedType) {

        VariableType usedType = type();

        assert usedType.equals(requestedType);

        return "(" + m_lhs.getCVC3Output(usedType) + " " + m_op.convertToCVC3Op() + " " + m_rhs.getCVC3Output(usedType) + ")";

    }

    

    MatlabExpression m_lhs, m_rhs;

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

+6 −2
Original line number Diff line number Diff line
@@ -20,8 +20,12 @@ public final class MatlabLiteral implements MatlabExpression, MatlabExpressionVa 
    }



    @Override

    public String getCVC3Output() {

    public String getCVC3Output(VariableType requestedType) {

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

            return m_value;

        } else {

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

        }

    }

    

    final String m_value;

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

+2 −1
Original line number Diff line number Diff line
@@ -27,7 +27,8 @@ public class Variable implements MatlabExpression, MatlabExpressionValue { 
    private VariableType m_type;



    @Override

    public String getCVC3Output() {

    public String getCVC3Output(VariableType requestedType) {

        assert m_type.equals(requestedType);

        return m_name;

    }

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

+2 −2
Original line number Diff line number Diff line
@@ -26,7 +26,7 @@ public class MatlabExpressionOperationTest { 
        String CVC3Output = "(a + b)";

        VariableType expressionType = new RealVariableType();

        

        assertEquals(CVC3Output, instance.getCVC3Output());

        assertEquals(CVC3Output, instance.getCVC3Output(instance.type()));

        assertEquals(expressionType, instance.type());

    }

    /**
@@ -44,7 +44,7 @@ public class MatlabExpressionOperationTest { 
        String CVC3Output = "(b + a)";

        VariableType expressionType = new RealVariableType();

        

        assertEquals(CVC3Output, instance.getCVC3Output());

        assertEquals(CVC3Output, instance.getCVC3Output(instance.type()));

        assertEquals(expressionType, instance.type());

    }