Implement fixed point + parsing. (d7050f47) · Commits · Curtis Milo / tet

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

0 → 100644

+69 −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
		*/
		final public class FixedPointVariableType implements VariableType {

		public FixedPointVariableType(boolean signed, int digits, int fractionPart) {
		m_isSigned = signed;
		m_digits = digits;
		m_fractionPart = fractionPart;
		}

		public boolean isSigned() {
		return m_isSigned;
		}

		public int digits() {
		return m_digits;
		}

		public int fractionPart() {
		return m_fractionPart;
		}

		@Override
		public String getCVC3Definition(String variableName) {
		return "BITVECTOR("+m_digits+")";
		}

		@Override
		public boolean canCastToType(VariableType type) {
		return false;
		}

		@Override
		public boolean equals(Object othero) {
		if(!(othero instanceof FixedPointVariableType)) {
		return false;
		} else {
		FixedPointVariableType other = (FixedPointVariableType)othero;
		if(other.m_isSigned == m_isSigned &&
		other.m_digits == m_digits &&
		other.m_fractionPart == m_fractionPart) {
		return true;
		} else {
		return false;
		}
		}
		}

		@Override
		public int hashCode() {
		int hash = 0;
		hash += (this.m_isSigned ? 1 : 0);
		hash = 2 * hash + this.m_fractionPart;
		hash = 83 * hash + this.m_digits;
		return hash;
		}

		private final int m_fractionPart;
		private final int m_digits;
		private final boolean m_isSigned;
		}

Matlab2SMT/src/main/java/ca/mcmaster/cas/matlab2smt/VariableParser.g4

+8 −2

Original line number	Diff line number	Diff line
		@@ -6,8 +6,14 @@ vartype: ':' type_info
		\| defaulttype;
		defaulttype: ;
		type_info: 'bool'
		\| 'real'
		\| 'fixed' ;
		\| real_type
		\| fixed_type ;

		real_type: 'real';

		fixed_type: 'fixedt(' NAT ',' NAT ')'
		\| 'fixedt(' NAT ',' NAT ',' NAT ')';

		ID: [a-zA-Z][a-zA-Z0-9]*; //Variable identifier. Start with letter, then alpha numerical allowed.
		NAT: [0-9]+;
		WS : [ \t\r\n]+ -> skip ; // skip spaces, tabs, newlines

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

+28 −1

Original line number	Diff line number	Diff line
		@@ -5,6 +5,8 @@
		package ca.mcmaster.cas.matlab2smt;

		import ca.mcmaster.cas.matlab2smt.VariableParserParser.DefaulttypeContext;
		import ca.mcmaster.cas.matlab2smt.VariableParserParser.Fixed_typeContext;
		import ca.mcmaster.cas.matlab2smt.VariableParserParser.Real_typeContext;
		import ca.mcmaster.cas.matlab2smt.VariableParserParser.VarContext;
		import java.util.HashMap;
		import java.util.Map;
		@@ -13,6 +15,7 @@ import org.antlr.v4.runtime.ANTLRInputStream;
		import org.antlr.v4.runtime.CommonTokenStream;
		import org.antlr.v4.runtime.tree.ParseTree;
		import org.antlr.v4.runtime.tree.ParseTreeWalker;
		import org.antlr.v4.runtime.tree.TerminalNode;

		/**
		*
		@@ -38,7 +41,14 @@ public class VariableParser {

		private void parseStringToVariables(String variables) {
		// create a CharStream that reads from standard input
		ANTLRInputStream input = new ANTLRInputStream(variables);
		ANTLRInputStream input = new ANTLRInputStream(variables) {

		@Override
		public int LA(int i) {
		return Character.toLowerCase(super.LA(i));
		}

		};

		// create a lexer that feeds off of input CharStream
		VariableParserLexer lexer = new VariableParserLexer(input);
		@@ -71,6 +81,23 @@ public class VariableParser {
		currentType = new RealVariableType();
		}

		@Override
		public void enterReal_type(Real_typeContext ctx) {
		currentType = new RealVariableType();
		}

		@Override
		public void enterFixed_type(Fixed_typeContext ctx) {
		boolean signed = (ctx.NAT(0).getText().equals("0"))?false:true;
		int digits = Integer.parseInt(ctx.NAT(1).getText());
		int fractionPart = 0;
		TerminalNode fractionNode;
		if ((fractionNode = ctx.NAT(2)) != null) {
		fractionPart = Integer.parseInt(fractionNode.getText());
		}
		currentType = new FixedPointVariableType(signed, digits, fractionPart);
		}

		@Override
		public void exitVar(VarContext ctx) {
		m_variables.put(currentName, new Variable(currentName, currentType));

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

0 → 100644

+54 −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;

		import org.junit.Test;
		import static org.junit.Assert.*;

		/**
		*
		* @author matthew
		*/
		public class FixedPointVariableTypeTest {
		/**
		* Test of constructor in class FixedPointType.
		*/
		@Test
		public void testConstructor() {
		FixedPointVariableType instance = new FixedPointVariableType(true, 19, 9);
		assertEquals(true, instance.isSigned());
		assertEquals(19, instance.digits());
		assertEquals(9, instance.fractionPart());
		}
		/**
		* Test of getCVC3Definition method, of class FixedPointType.
		*/
		@Test
		public void testGetCVC3Definition() {
		FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8);
		assertEquals("BITVECTOR(16)", instance.getCVC3Definition(null));
		}

		/**
		* Test of canCastToType method, of class FixedPointType.
		*/
		@Test
		public void testCanCastToType() {
		FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8);
		assertFalse(instance.canCastToType(new RealVariableType()));
		}

		/**
		* Test of equals method, of class FixedPointType.
		*/
		@Test
		public void testEquals() {
		FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8);
		assertEquals(new FixedPointVariableType(true, 16, 8), instance);
		assertFalse(instance.equals(new FixedPointVariableType(false, 16, 8)));
		assertFalse(instance.equals(new FixedPointVariableType(true, 15, 8)));
		assertFalse(instance.equals(new FixedPointVariableType(true, 16, 7)));
		}
		}

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

+48 −0

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

		import ca.mcmaster.cas.matlab2smt.FixedPointVariableType;
		import ca.mcmaster.cas.matlab2smt.RealVariableType;
		import ca.mcmaster.cas.matlab2smt.Variable;
		import ca.mcmaster.cas.matlab2smt.VariableParser;
		@@ -28,6 +29,45 @@ public class VariableParserTest {
		assertEquals(new RealVariableType(), a.type());
		}
		@Test
		public void testRealVariable() {
		VariableParser vars = new VariableParser("a: real");
		Variable a = vars.getVar("a");
		assertEquals("a", a.name());
		assertEquals(new RealVariableType(), a.type());
		}
		@Test
		public void testFixedPointNoDecimalVariable() {
		VariableParser vars = new VariableParser("a: fixedt(1, 16)");
		Variable a = vars.getVar("a");
		FixedPointVariableType type = (FixedPointVariableType)a.type();
		assertEquals("a", a.name());
		assertNotNull(type);
		assertEquals(true, type.isSigned());
		assertEquals(16, type.digits());
		assertEquals(0, type.fractionPart());

		vars = new VariableParser("a: fixedt(0, 15, 4)");
		a = vars.getVar("a");
		type = (FixedPointVariableType)a.type();
		assertEquals("a", a.name());
		assertNotNull(type);
		assertEquals(false, type.isSigned());
		assertEquals(15, type.digits());
		assertEquals(4, type.fractionPart());
		}
		@Test
		public void testCaseInsensitivtySearch() {
		VariableParser vars = new VariableParser("a: ReAl");
		Variable a = vars.getVar("a");
		assertEquals("a", a.name());
		assertEquals(new RealVariableType(), a.type());

		vars = new VariableParser("A: REAL");
		a = vars.getVar("A");
		assertEquals("A", a.name());
		assertEquals(new RealVariableType(), a.type());
		}
		@Test
		public void testMultiVariableOutput() {
		VariableParser vars = new VariableParser("a,b");
		try {
		@@ -36,5 +76,13 @@ public class VariableParserTest {
		//Depending upon maps sort order, either a or be may be first. Either is correct, so if the first test fails, retry with order reversed.
		assertEquals("b:REAL;\na:REAL;\n", vars.getCVC3Output());
		}

		vars = new VariableParser("a:fixedt(1,16,9),b");
		try {
		assertEquals("a:BITVECTOR(16);\nb:REAL\n;", vars.getCVC3Output());
		} catch(AssertionError e) {
		//Depending upon maps sort order, either a or be may be first. Either is correct, so if the first test fails, retry with order reversed.
		assertEquals("b:REAL;\na:BITVECTOR(16);\n", vars.getCVC3Output());
		}
		}
		}