Working fixed point output. (2f0530cd) · Commits · Curtis Milo / tet

Matlab2SMT/pom.xml

+5 −0

Original line number	Diff line number	Diff line
		@@ -26,6 +26,11 @@
		<artifactId>antlr4-runtime</artifactId>
		<version>4.0</version>
		</dependency>
		<dependency>
		<groupId>org.apache.commons</groupId>
		<artifactId>commons-lang3</artifactId>
		<version>3.1</version>
		</dependency>
		</dependencies>

		<build>

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

+8 −1

Original line number	Diff line number	Diff line
		@@ -43,7 +43,14 @@ final class MatlabExpressionOperation implements MatlabExpression {
		public String getCVC3Output(VariableType requestedType) {
		VariableType usedType = type();
		assert usedType.equals(requestedType);
		return "(" + m_lhs.getCVC3Output(usedType) + " " + m_op.convertToCVC3Op() + " " + m_rhs.getCVC3Output(usedType) + ")";
		switch (m_op.CVC3OpTypeForType(usedType)) {
		case CenterOp:
		return "(" + m_lhs.getCVC3Output(usedType) + " " + m_op.convertToCVC3Op(usedType) + " " + m_rhs.getCVC3Output(usedType) + ")";
		case Function:
		return m_op.convertToCVC3Op(usedType) + m_lhs.getCVC3Output(usedType) + "," + m_rhs.getCVC3Output(usedType) + ")";
		default:
		throw new IllegalStateException("Cannot output expression operation for requested operation type.");
		}
		}

		MatlabExpression m_lhs, m_rhs;

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

+24 −1

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

		import java.math.BigDecimal;
		import java.math.BigInteger;
		import org.apache.commons.lang3.StringUtils;

		/**
		*
		* @author matthew
		@@ -23,6 +27,24 @@ public final class MatlabLiteral implements MatlabExpression, MatlabExpressionVa
		public String getCVC3Output(VariableType requestedType) {
		if (requestedType instanceof RealVariableType \|\| requestedType instanceof LiteralNumberType) {
		return m_value;
		} else if (requestedType instanceof FixedPointVariableType) {
		FixedPointVariableType type = (FixedPointVariableType)requestedType;
		BigDecimal decimal = new BigDecimal(m_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 "0bit" + StringUtils.repeat('1', type.digits() - bits.length()) + bits;
		} else {
		return "0bit" + StringUtils.repeat('0', type.digits() - bits.length()) + bits;
		}
		} else {
		throw new IllegalArgumentException("Can't cast literal to that type!");
		}
		@@ -50,7 +72,8 @@ public final class MatlabLiteral implements MatlabExpression, MatlabExpressionVa

		@Override
		public boolean canCastToType(VariableType type) {
		return type instanceof RealVariableType;
		return type instanceof RealVariableType \|\|
		type instanceof FixedPointVariableType;
		}

		@Override

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

+32 −8

Original line number	Diff line number	Diff line
		@@ -9,9 +9,9 @@ package ca.mcmaster.cas.matlab2smt;
		* @author matthew
		*/
		enum MatlabOperation {
		Addition("+"),
		GreaterThen(">"),
		Equals("=");
		Addition("+", "BVPLUS("),
		GreaterThen(">", "BVSGT("),
		Equals("=", "=");

		static MatlabOperation getOpForSymbol(String text) {
		if(text.equals("+")) {
		@@ -25,13 +25,37 @@ enum MatlabOperation {
		}
		}

		MatlabOperation(String CVC3Version){
		m_CVC3Version = CVC3Version;
		MatlabOperation(String CVC3VersionCenter, String CVC3VersionFunction){
		m_CVC3VersionCenter = CVC3VersionCenter;
		m_CVC3VersionFunction = CVC3VersionFunction;
		}

		String convertToCVC3Op(){
		return m_CVC3Version;
		String convertToCVC3Op(VariableType type){
		switch(CVC3OpTypeForType(type)) {
		case Function:
		if(this == Addition && type instanceof FixedPointVariableType) {
		FixedPointVariableType typeF = (FixedPointVariableType)type;
		return m_CVC3VersionFunction + typeF.digits() + ",";
		} else {
		return m_CVC3VersionFunction;
		}
		case CenterOp:
		return m_CVC3VersionCenter;
		default:
		throw new IllegalStateException("CVC3 Operation type asked for that doesn't exist!");
		}
		}

		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_CVC3Version;
		String m_CVC3VersionCenter, m_CVC3VersionFunction;
		}

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

0 → 100644

+16 −0

Original line number	Diff line number	Diff line
		/*
		* To change this template, choose Tools \| Templates
		* and open the template in the editor.
		*/
		package ca.mcmaster.cas.matlab2smt;

		/**
		*
		* @author matthew
		*/
		public enum OperationType {
		CenterOp,
		PrefixOp,
		PostfixOp,
		Function;
		}