Split the SALVariablesDeclarationGenerator from SALExpressionGenerator. (544ce6ad) · Commits · tables / jtet

src/main/java/ca/mcscert/jtet/salgenerator/SALExpressionGenerator.java

+2 −37

Original line number	Diff line number	Diff line
		@@ -35,7 +35,8 @@ import java.util.Map;
		/**
		* @author Matthew Dawson <matthew@mjdsystems.ca>
		*/
		public class SALExpressionGenerator implements VariablesDeclarationGenerator, ExpressionGenerator {
		public class SALExpressionGenerator implements ExpressionGenerator {
		public final static SALExpressionGenerator Generator = new SALExpressionGenerator();

		private static String GetInfixSymbolFor(BinaryOperation op) {
		switch (op) {
		@@ -91,42 +92,6 @@ public class SALExpressionGenerator implements VariablesDeclarationGenerator, Ex
		return "(" + GetUnaryOperationSymbolFor(op) + " " + expression + ")";
		}

		public String GenerateVariableType(VariableType type) {
		if (type instanceof RealVariableType) {
		return "REAL";
		} else if (type instanceof BooleanVariableType) {
		return "BOOLEAN";
		} else {
		throw new IllegalArgumentException("The SAL Generator doesn't currently handle this variable type (Class: " + type.getClass().getName() + ")");
		}
		}

		@Override
		public String GenerateVariablesDeclaration(VariableCollection variableCollection) {
		Map<String, Variable> vars = variableCollection.getVariables();
		StringBuilder ret = new StringBuilder();

		// Generate all the variables.
		for(Variable var : vars.values()) {
		ret.append(var.outputName()).append(":");
		VariableType type = var.type();
		if (type.subtypePredicate() == null) {
		ret.append(GenerateVariableType(type));
		} else {
		ret.append("{")
		.append(var.outputName())
		.append(":")
		.append(GenerateVariableType(type))
		.append("\|")
		.append(type.subtypePredicate().getCheckerOutput(this, BooleanVariableType.Type))
		.append("}");
		}
		ret.append("\n");
		}

		return ret.toString();
		}

		@Override
		public String GenerateLiteralValue(String value, VariableType requestedType) {
		if (requestedType instanceof RealVariableType) {

src/main/java/ca/mcscert/jtet/salgenerator/SALVariablesDeclarationGenerator.java

0 → 100644

+76 −0

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2014 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.salgenerator;

		import ca.mcscert.jtet.expression.*;

		import java.util.Map;

		/**
		* @author Matthew Dawson <matthew@mjdsystems.ca>
		*/
		public class SALVariablesDeclarationGenerator implements VariablesDeclarationGenerator {
		public final static SALVariablesDeclarationGenerator Generator = new SALVariablesDeclarationGenerator();

		@Override
		public String GenerateVariablesDeclaration(VariableCollection variableCollection) {
		Map<String, Variable> vars = variableCollection.getVariables();
		StringBuilder ret = new StringBuilder();

		// Generate all the variables.
		for(Variable var : vars.values()) {
		ret.append(var.outputName()).append(":");
		VariableType type = var.type();
		if (type.subtypePredicate() == null) {
		ret.append(GenerateVariableType(type));
		} else {
		ret.append("{")
		.append(var.outputName())
		.append(":")
		.append(GenerateVariableType(type))
		.append("\|")
		.append(type.subtypePredicate().getCheckerOutput(SALExpressionGenerator.Generator, BooleanVariableType.Type))
		.append("}");
		}
		ret.append("\n");
		}

		return ret.toString();
		}

		public String GenerateVariableType(VariableType type) {
		if (type instanceof RealVariableType) {
		return "REAL";
		} else if (type instanceof BooleanVariableType) {
		return "BOOLEAN";
		} else {
		throw new IllegalArgumentException("The SAL Generator doesn't currently handle this variable type (Class: " + type.getClass().getName() + ")");
		}
		}
		}

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

+2 −2

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

		import ca.mcscert.jtet.cvc3generator.CVC3VariablesDeclarationGenerator;
		import ca.mcscert.jtet.parsers.VariableParser;
		import ca.mcscert.jtet.salgenerator.SALExpressionGenerator;
		import ca.mcscert.jtet.salgenerator.SALVariablesDeclarationGenerator;
		import ca.mcscert.jtet.smtlibchecker.SMTLIBVariablesDeclarationGenerator;
		import org.junit.Before;
		import org.junit.Test;
		@@ -97,7 +97,7 @@ public class GenericVariablesDeclarationGeneratorTest {
		null,
		null
		},
		{new SALExpressionGenerator(),
		{new SALVariablesDeclarationGenerator(),
		"x:REAL\n",
		"new_x_name:REAL\n",
		"x:{x:REAL\|(x > 0)}\n",