Add support for generating enumeration types. (46d66936) · Commits · tables / tet

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/CVC3Generator.java

+25 −1

Original line number	Diff line number	Diff line
		@@ -6,7 +6,9 @@ package ca.mcmaster.cas.tabularexpressiontoolbox.expression;

		import java.math.BigDecimal;
		import java.math.BigInteger;
		import java.util.HashSet;
		import java.util.Map;
		import java.util.Set;

		import org.apache.commons.lang3.StringUtils;

		@@ -188,6 +190,8 @@ final public class CVC3Generator implements CheckerGenerator{
		return "BITVECTOR(" + ((FixedPointVariableType) type).digits() + ")";
		} else if (type instanceof BooleanVariableType) {
		return "BOOLEAN";
		} else if (type instanceof EnumerationVariableType) {
		return ((EnumerationVariableType) type).name();
		} else {
		throw new IllegalArgumentException("CVC3 Doesn't handle this variable type (Class: " + type.getClass().getName() + ")");
		}
		@@ -196,9 +200,29 @@ final public class CVC3Generator implements CheckerGenerator{
		@Override
		public String GenerateVariablesDeclaration(VariableCollection variableCollection) {
		Map<String, Variable> vars = variableCollection.getVariables();
		Set<EnumerationVariableType> emittedEnumerations = new HashSet<EnumerationVariableType>();

		StringBuilder ret = new StringBuilder();
		// First generate all the variables.
		// First generate all the enumeration types.
		for(Variable var : vars.values()) {
		if (var.type() instanceof EnumerationVariableType && !emittedEnumerations.contains(var.type())) {
		ret.append("DATATYPE\n ")
		.append(((EnumerationVariableType) var.type()).name())
		.append(" = ");

		boolean firstValue = false;
		for(String enumValue : ((EnumerationVariableType) var.type()).enumerationValues()) {
		if (firstValue == true) {
		ret.append(" \| ");
		}
		firstValue = true;
		ret.append(enumValue);
		}
		ret.append("\nEND;\n");
		}
		}

		// Then generate all the variables.
		for(Variable var : vars.values()) {
		ret.append(var.name())
		.append(":")

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/SMTLIBGenerator.java

+56 −1

Original line number	Diff line number	Diff line
		@@ -16,7 +16,9 @@
		*/
		package ca.mcmaster.cas.tabularexpressiontoolbox.expression;

		import java.util.HashSet;
		import java.util.Map;
		import java.util.Set;

		/**
		*
		@@ -49,15 +51,66 @@ public class SMTLIBGenerator implements CheckerGenerator {
		@Override
		public String GenerateVariablesDeclaration(VariableCollection variableCollection) {
		Map<String, Variable> vars = variableCollection.getVariables();
		Set<EnumerationVariableType> emittedEnumerations = new HashSet<EnumerationVariableType>();

		StringBuilder ret = new StringBuilder();
		// First generate all the variables.
		// First generate all the enumeration types.
		for(Variable var : vars.values()) {
		if (var.type() instanceof EnumerationVariableType && !emittedEnumerations.contains(var.type())) {
		// For each enumeration, first emit the actual enumeration type name.
		EnumerationVariableType enumType = (EnumerationVariableType)var.type();
		ret.append("(declare-sort ")
		.append(enumType.name())
		.append(" 0)\n");

		// Next, emit the enumeration values, using the enumeration type.
		for(String enumValue : enumType.enumerationValues()) {
		ret.append("(declare-fun ")
		.append(enumValue)
		.append(" () ")
		.append(enumType.name())
		.append(")\n");
		}

		// Restrict the enumeration values so that they are all considered different.
		ret.append("(assert (distinct");
		for(String enumValue : enumType.enumerationValues()) {
		ret.append(" ")
		.append(enumValue);
		}
		ret.append("))\n");

		// Finally, emit a function that ensure any enumeration variable can only be the values given.
		ret.append("(define-fun is")
		.append(enumType.name())
		.append(" ((val ")
		.append(enumType.name())
		.append(")) Bool (or");
		for(String enumValue : enumType.enumerationValues()) {
		ret.append(" (= val ")
		.append(enumValue)
		.append(")");
		}
		ret.append("))\n");
		}
		}

		// Then generate all the variables.
		for (Variable var : vars.values()) {
		ret.append("(declare-fun ")
		.append(var.name())
		.append(" () ")
		.append(GenerateVariableType(var.type()))
		.append(")\n");

		// If variable is an enumeration, make sure that it is limited to only enumeration values.
		if (var.type() instanceof EnumerationVariableType) {
		ret.append("(assert (is")
		.append(((EnumerationVariableType) var.type()).name())
		.append(" ")
		.append(var.name())
		.append("))\n");
		}
		}

		// Then generate the variable predicates. This ensures any dependent variables are declared.
		@@ -76,6 +129,8 @@ public class SMTLIBGenerator implements CheckerGenerator {
		return "Real";
		} else if (type instanceof BooleanVariableType) {
		return "Bool";
		} else if (type instanceof EnumerationVariableType) {
		return ((EnumerationVariableType) type).name();
		} else {
		throw new IllegalArgumentException("SMT-LIB Doesn't handle this variable type (Class: " + type.getClass().getName() + ")");
		}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/GenericVariableDeclarationGeneratorTest.java

0 → 100644

+122 −0

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
		*
		* This program is free software: you can redistribute it and/or modify
		* it under the terms of the GNU General Public License as published by
		* the Free Software Foundation, either version 3 of the License, or
		* (at your option) any later version.
		*
		* This program is distributed in the hope that it will be useful,
		* but WITHOUT ANY WARRANTY; without even the implied warranty of
		* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
		* GNU General Public License for more details.
		*
		* You should have received a copy of the GNU General Public License
		* along with this program. If not, see <http://www.gnu.org/licenses/>.
		*/
		package ca.mcmaster.cas.tabularexpressiontoolbox.expression;

		import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParser;
		import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser;
		import org.junit.Before;
		import org.junit.Test;
		import org.junit.runner.RunWith;
		import org.junit.runners.Parameterized;
		import org.junit.runners.Parameterized.Parameter;
		import org.junit.runners.Parameterized.Parameters;

		import java.util.Arrays;
		import java.util.Collection;
		import java.util.LinkedHashSet;
		import java.util.Map;

		import static org.junit.Assert.*;

		/**
		* @author Matthew Dawson <matthew@mjdsystems.ca>
		*/
		@RunWith(Parameterized.class)
		public class GenericVariableDeclarationGeneratorTest {
		@Parameters
		public static Collection<Object[]> data() {
		return Arrays.asList(new Object[][]{
		{new SMTLIBGenerator(),
		"(declare-fun x () Real)\n",
		null,
		null,
		"(declare-sort MyEnum 0)\n" +
		"(declare-fun e1 () MyEnum)\n" +
		"(declare-fun e2 () MyEnum)\n" +
		"(declare-fun e3 () MyEnum)\n" +
		"(assert (distinct e1 e2 e3))\n" +
		"(define-fun isMyEnum ((val MyEnum)) Bool (or (= val e1) (= val e2) (= val e3)))\n" +
		"(declare-fun x () MyEnum)\n" +
		"(assert (isMyEnum x))\n"
		},
		{new CVC3Generator(),
		"x:REAL;\n",
		"x:BITVECTOR(8);\n",
		"x:BITVECTOR(8);\n",
		"DATATYPE\n MyEnum = e1 \| e2 \| e3\nEND;\nx:MyEnum;\n"
		}
		});
		}
		@Parameter(value = 0)
		public CheckerGenerator generator;

		@Parameter(value = 1)
		public String RealExpectedOutput;

		@Parameter(value = 2)
		public String SignedFixedPointExpectedOutput;

		@Parameter(value = 3)
		public String UnsignedFixedPointExpectedOutput;

		@Parameter(value = 4)
		public String EnumerationExpectedOutput;

		@Test
		public void RealTest() {
		if (RealExpectedOutput != null) {
		VariableCollection vars = variableParser.parseVariables("x");
		assertEquals(RealExpectedOutput, generator.GenerateVariablesDeclaration(vars));
		}
		}

		@Test
		public void SignedFixedPointTest() {
		if (SignedFixedPointExpectedOutput != null) {
		VariableCollection vars = variableParser.parseVariables("x:fixedt(1, 8, 2)");
		assertEquals(SignedFixedPointExpectedOutput, generator.GenerateVariablesDeclaration(vars));
		}
		}

		@Test
		public void UnsignedFixedPointTest() {
		if (UnsignedFixedPointExpectedOutput != null) {
		VariableCollection vars = variableParser.parseVariables("x:fixedt(0, 8, 2)");
		assertEquals(UnsignedFixedPointExpectedOutput, generator.GenerateVariablesDeclaration(vars));
		}
		}

		@Test
		public void SingleVariableSingleEnumerationTest() {
		if (EnumerationExpectedOutput != null) {
		VariableCollection vars = variableParser.parseVariables("x:MyEnum");
		assertEquals(EnumerationExpectedOutput, generator.GenerateVariablesDeclaration(vars));
		}
		}

		@Before
		public void SetupVariableParser() {
		EnumerationVariableType myEnum = new EnumerationVariableType("MyEnum");
		myEnum.enumerationValues().add("e1");
		myEnum.enumerationValues().add("e2");
		myEnum.enumerationValues().add("e3");

		variableParser.addCustomType("MyEnum", myEnum);
		}

		VariableParser variableParser = new VariableParser();
		}