Rename CVC3Generator to CVC3ExpressionGenerator. (dfdda6a6) · Commits · tables / jtet

src/main/java/ca/mcscert/jtet/expression/CVC3Generator.java→src/main/java/ca/mcscert/jtet/cvc3generator/CVC3ExpressionGenerator.java

+10 −10

Original line number	Diff line number	Diff line
		@@ -2,7 +2,7 @@
		* To change this template, choose Tools \| Templates
		* and open the template in the editor.
		*/
		package ca.mcscert.jtet.expression;
		package ca.mcscert.jtet.cvc3generator;

		import java.math.BigDecimal;
		import java.math.BigInteger;
		@@ -10,14 +10,14 @@ import java.util.HashSet;
		import java.util.Map;
		import java.util.Set;

		import ca.mcscert.jtet.expression.*;
		import org.apache.commons.lang3.StringUtils;

		/**
		*
		* @author matthew
		*/
		final public class CVC3Generator implements VariablesDeclarationGenerator, ExpressionGenerator {

		final public class CVC3ExpressionGenerator implements VariablesDeclarationGenerator, ExpressionGenerator {
		// For operations that don't have specific signed/unsigned representations, use this function.
		private static String GetIndifferentFixedPointFunctionFor(BinaryOperation op) {
		switch (op) {
		@@ -97,7 +97,7 @@ final public class CVC3Generator implements VariablesDeclarationGenerator, Expre
		throw new RuntimeException("Should never happen!");
		}

		protected static String ConvertToOutputOp(BinaryOperation op, VariableType type) {
		public static String ConvertToOutputOp(BinaryOperation op, VariableType type) {
		switch (OpTypeForVariableType(op, type)) {
		case Function:
		String func = GetSignedFixedPointFunctionFor(op);
		@@ -130,11 +130,11 @@ final public class CVC3Generator implements VariablesDeclarationGenerator, Expre

		@Override
		public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType) {
		switch (CVC3Generator.OpTypeForVariableType(op, usedType)) {
		switch (CVC3ExpressionGenerator.OpTypeForVariableType(op, usedType)) {
		case CenterOp:
		return "(" + lhsExp + " " + CVC3Generator.ConvertToOutputOp(op, usedType) + " " + rhsExp + ")";
		return "(" + lhsExp + " " + CVC3ExpressionGenerator.ConvertToOutputOp(op, usedType) + " " + rhsExp + ")";
		case Function:
		return CVC3Generator.ConvertToOutputOp(op, usedType) + lhsExp + "," + rhsExp + ")";
		return CVC3ExpressionGenerator.ConvertToOutputOp(op, usedType) + lhsExp + "," + rhsExp + ")";
		default:
		throw new IllegalStateException("Cannot output expression operation for requested operation type.");
		}
		@@ -152,11 +152,11 @@ final public class CVC3Generator implements VariablesDeclarationGenerator, Expre

		@Override
		public String GenerateUnaryOperation(UnaryOperation op, String expression, VariableType usedType) {
		switch (CVC3Generator.OpTypeForVariableType(op, usedType)) {
		switch (CVC3ExpressionGenerator.OpTypeForVariableType(op, usedType)) {
		case PrefixOp:
		return "(" + CVC3Generator.ConvertToOutputOp(op, usedType) + " " + expression + ")";
		return "(" + CVC3ExpressionGenerator.ConvertToOutputOp(op, usedType) + " " + expression + ")";
		case Function:
		return CVC3Generator.ConvertToOutputOp(op, usedType) + "(" + expression + ")";
		return CVC3ExpressionGenerator.ConvertToOutputOp(op, usedType) + "(" + expression + ")";
		default:
		throw new IllegalStateException("Cannot output expression operation for requested operation type.");
		}

src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java

+3 −3

Original line number	Diff line number	Diff line
		@@ -109,7 +109,7 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridChec
		if (m_currentlyRunning) {
		outputCells();
		}
		m_parentCellsCVC3Code.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, BooleanVariableType.Type));
		m_parentCellsCVC3Code.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3ExpressionGenerator, BooleanVariableType.Type));
		m_currentlyRunning = true;
		}

		@@ -129,7 +129,7 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridChec
		@Override
		public void handleLeafCell(Cell cell) {
		// First get the appropriate CVC3 code from matlab. Capture generation for further processing.
		ExpressionGeneratorSpy spy = new ExpressionGeneratorSpy(m_CVC3Generator);
		ExpressionGeneratorSpy spy = new ExpressionGeneratorSpy(m_CVC3ExpressionGenerator);
		String newCellCode = MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(spy, BooleanVariableType.Type);

		// Next, find all the fixed point expressions and handle them.
		@@ -256,5 +256,5 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridChec

		// To fix properly.
		VariableCollection m_variableDefinitions;
		CVC3Generator m_CVC3Generator = new CVC3Generator();
		CVC3ExpressionGenerator m_CVC3ExpressionGenerator = new CVC3ExpressionGenerator();
		}

src/test/java/ca/mcscert/jtet/expression/CVC3GeneratorTest.java→src/test/java/ca/mcscert/jtet/cvc3generator/CVC3ExpressionGeneratorTest.java

+9 −5

Original line number	Diff line number	Diff line
		@@ -2,8 +2,12 @@
		* To change this template, choose Tools \| Templates
		* and open the template in the editor.
		*/
		package ca.mcscert.jtet.expression;
		package ca.mcscert.jtet.cvc3generator;

		import ca.mcscert.jtet.expression.BinaryOperation;
		import ca.mcscert.jtet.expression.FixedPointVariableType;
		import ca.mcscert.jtet.expression.Literal;
		import ca.mcscert.jtet.expression.RealVariableType;
		import org.junit.Test;
		import org.junit.runner.RunWith;
		import org.junit.runners.JUnit4;
		@@ -14,15 +18,15 @@ import static org.junit.Assert.*;
		* @author matthew
		*/
		@RunWith(JUnit4.class)
		public class CVC3GeneratorTest {
		public class CVC3ExpressionGeneratorTest {
		/**
		* Test of addition operation.
		*/
		@Test
		public void testAdditionOpConverstion() {
		BinaryOperation op = BinaryOperation.Addition;
		assertEquals("+", CVC3Generator.ConvertToOutputOp(op, RealVariableType.Type));
		assertEquals("BVPLUS(13,", CVC3Generator.ConvertToOutputOp(op, new FixedPointVariableType(true, 13, 5)));
		assertEquals("+", CVC3ExpressionGenerator.ConvertToOutputOp(op, RealVariableType.Type));
		assertEquals("BVPLUS(13,", CVC3ExpressionGenerator.ConvertToOutputOp(op, new FixedPointVariableType(true, 13, 5)));
		}
		/**
		* Test of literals containing decimals.
		@@ -32,6 +36,6 @@ public class CVC3GeneratorTest {
		@Test
		public void testLiteralRationalsAreFractions() {
		Literal literal = new Literal("4.56");
		assertEquals("(456/100)", literal.getCheckerOutput(new CVC3Generator(), RealVariableType.Type));
		assertEquals("(456/100)", literal.getCheckerOutput(new CVC3ExpressionGenerator(), RealVariableType.Type));
		}
		}

src/test/java/ca/mcscert/jtet/expression/EnumerationVariableTypeGenerationTest.java

+2 −1

Original line number	Diff line number	Diff line
		@@ -28,6 +28,7 @@
		*/
		package ca.mcscert.jtet.expression;

		import ca.mcscert.jtet.cvc3generator.CVC3ExpressionGenerator;
		import ca.mcscert.jtet.parsers.PVSSimpleParser;
		import ca.mcscert.jtet.parsers.VariableParser;
		import org.junit.Before;
		@@ -54,7 +55,7 @@ public class EnumerationVariableTypeGenerationTest {
		"(= x e1)",
		"(distinct x e1)",
		},
		{new CVC3Generator(),
		{new CVC3ExpressionGenerator(),
		"(x = e1)",
		"(x /= e1)",
		}

src/test/java/ca/mcscert/jtet/expression/FixedPointVariableTypeTest.java

+2 −1

Original line number	Diff line number	Diff line
		@@ -4,6 +4,7 @@
		*/
		package ca.mcscert.jtet.expression;

		import ca.mcscert.jtet.cvc3generator.CVC3ExpressionGenerator;
		import org.junit.Test;
		import org.junit.runner.RunWith;
		import org.junit.runners.JUnit4;
		@@ -31,7 +32,7 @@ public class FixedPointVariableTypeTest {
		*/
		@Test
		public void testGetCVC3Definition() {
		CVC3Generator generator = new CVC3Generator();
		CVC3ExpressionGenerator generator = new CVC3ExpressionGenerator();
		FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8);
		assertEquals("BITVECTOR(16)", generator.GenerateVariableType(instance));
		}