Create a new SMTLIBTypeDeclarationGenerator. (16d392a1) · Commits · tables / jtet

src/main/java/ca/mcscert/jtet/smtlibchecker/SMTLIBTypeDeclarationGenerator.java

0 → 100644

+91 −0

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
		*
		* Redistribution and use in source and binary forms, with or without
		* modification, are permitted provided that the following conditions are
		* met:
		*
		* * Redistributions of source code must retain the above copyright
		* notice, this list of conditions and the following disclaimer.
		* * Redistributions in binary form must reproduce the above copyright
		* notice, this list of conditions and the following disclaimer in
		* the documentation and/or other materials provided with the distribution
		* * Neither the name of the McMaster Centre for Software Certification nor the names
		* of its contributors may be used to endorse or promote products derived
		* from this software without specific prior written permission.
		*
		* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
		* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
		* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
		* ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
		* LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
		* CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
		* SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
		* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
		* CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
		* ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
		* POSSIBILITY OF SUCH DAMAGE.
		*/
		package ca.mcscert.jtet.smtlibchecker;

		import ca.mcscert.jtet.expression.EnumerationVariableType;
		import ca.mcscert.jtet.expression.TypeDeclarationGenerator;
		import ca.mcscert.jtet.expression.VariableType;

		import java.util.Set;

		/**
		*
		* @author Matthew Dawson
		* @author Yanjun Jiang
		*/
		public class SMTLIBTypeDeclarationGenerator implements TypeDeclarationGenerator {
		public final static SMTLIBTypeDeclarationGenerator Generator = new SMTLIBTypeDeclarationGenerator();

		@Override
		public String GenerateTypeDeclaration(Set<VariableType> types) {
		StringBuilder ret = new StringBuilder();
		//Generate all the enumeration types.
		for(VariableType type : types) {
		if (type instanceof EnumerationVariableType) {
		// For each enumeration, first emit the actual enumeration type name.
		EnumerationVariableType enumType = (EnumerationVariableType) 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");
		}
		}

		return ret.toString();
		}
		}

src/main/java/ca/mcscert/jtet/smtlibchecker/SMTLIBVariablesDeclarationGenerator.java

+1 −47

Original line number	Diff line number	Diff line
		@@ -30,9 +30,7 @@ package ca.mcscert.jtet.smtlibchecker;

		import ca.mcscert.jtet.expression.*;

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

		/**
		*
		@@ -44,53 +42,9 @@ public class SMTLIBVariablesDeclarationGenerator implements VariablesDeclaration
		@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 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");

		emittedEnumerations.add(enumType);
		}
		}

		// Then generate all the variables.
		//Generate all the variables.
		for (Variable var : vars.values()) {
		ret.append("(declare-fun ")
		.append(var.outputName())

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

+10 −1

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

		import ca.mcscert.jtet.cvc3generator.CVC3TypeDeclarationGenerator;
		import ca.mcscert.jtet.smtlibchecker.SMTLIBTypeDeclarationGenerator;
		import org.junit.Test;
		import org.junit.runner.RunWith;
		import org.junit.runners.Parameterized;
		@@ -50,7 +51,15 @@ public class GenericTypeDeclarationGeneratorTest {
		return Arrays.asList(new Object[][]{
		{new CVC3TypeDeclarationGenerator(),
		"DATATYPE\n Enum1 = e1 \| e2 \| e3\nEND;\n",
		}
		},
		{new SMTLIBTypeDeclarationGenerator(),
		"(declare-sort Enum1 0)\n" +
		"(declare-fun e1 () Enum1)\n" +
		"(declare-fun e2 () Enum1)\n" +
		"(declare-fun e3 () Enum1)\n" +
		"(assert (distinct e1 e2 e3))\n" +
		"(define-fun isEnum1 ((val Enum1)) Bool (or (= val e1) (= val e2) (= val e3)))\n",
		},
		});
		}
		@Parameter(value = 0)

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

+3 −21

Original line number	Diff line number	Diff line
		@@ -57,28 +57,10 @@ public class GenericVariablesDeclarationGeneratorTest {
		"(declare-fun x () Bool)\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",
		"(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 new_x_name () MyEnum)\n" +
		"(assert (isMyEnum new_x_name))\n",
		"(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" +
		"(declare-fun y () MyEnum)\n" +