Commit d802af4d authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add support for the enumeration into the generators with tests. 

Add support for the generators to deal with enumeration types properly, along
with making sure they won't generate output for other types of operations.
Currently only addition is checked.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@11088 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent f392484e

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

+7 −1
Original line number Diff line number Diff line
@@ -38,6 +38,11 @@ public enum BinaryOperation { 
                throw new IllegalArgumentException("Boolean operators and comparisons require a boolean output type!");

            }

        }

        if (outputType instanceof  EnumerationVariableType) {

            if (this != Equals && this != NotEquals) {

                throw new IllegalArgumentException("Enumeration types can only be checked for equality!");

            }

        }



        // Comparisions produce boolean outputs!

        switch(this) {
@@ -45,9 +50,10 @@ public enum BinaryOperation { 
            case GreaterThenEqual:

            case LessThen:

            case LessThenEqual:

                return Arrays.asList(new VariableTypeMarker[]{new RealVariableType(), new FixedPointVariableType.Marker()});

            case Equals:

            case NotEquals:

                return Arrays.asList(new VariableTypeMarker[]{new RealVariableType(), new FixedPointVariableType.Marker()});

                return Arrays.asList(new VariableTypeMarker[]{new RealVariableType(), new FixedPointVariableType.Marker(), new EnumerationVariableType.Marker()});

        }

        return Arrays.asList(new VariableTypeMarker[]{outputType});

    }

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

0 → 100644
+94 −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.Map;



import static org.junit.Assert.*;



/**

 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

@RunWith(Parameterized.class)

public class EnumerationVariableTypeGenerationTest {

    @Parameters

    public static Collection<Object[]> data() {

        return Arrays.asList(new Object[][]{

                {new SMTLIBGenerator(),

                        "(= x e1)",

                        "(distinct x e1)",

                },

                {new CVC3Generator(),

                        "(x = e1)",

                        "(x /= e1)",

                }

        });

    }



    static private VariableType outputType = new BooleanVariableType();



    @Parameter(value = 0)

    public CheckerGenerator generator;



    @Parameter(value = 1)

    public String EqualExpectedOutput;



    @Parameter(value = 2)

    public String NotEqualExpectedOutput;



    @Before

    public void setUp() throws Exception {

        EnumerationVariableType enumType = new EnumerationVariableType();

        enumType.enumerationValues().add("e1");



        variableParser.addCustomType("enum", enumType);

    }



    @Test

    public void EqualTest() {

        VariableCollection vars = variableParser.parseVariables("x:enum");

        Expression expr = PVSSimpleParser.parsePVSCode(vars, "x = e1");

        assertEquals(EqualExpectedOutput, expr.getCheckerOutput(generator, outputType));

    }



    @Test

    public void NotEqualTest() {

        VariableCollection vars = variableParser.parseVariables("x:enum");

        Expression expr = PVSSimpleParser.parsePVSCode(vars, "x /= e1");

        assertEquals(NotEqualExpectedOutput, expr.getCheckerOutput(generator, outputType));

    }



    @Test(expected=IllegalArgumentException.class)

    public void OtherOperatorsFailTest() {

        VariableCollection vars = variableParser.parseVariables("x:enum");

        Expression expr = PVSSimpleParser.parsePVSCode(vars, "x + e1");

        expr.getCheckerOutput(generator, vars.getVariables().get("x").type());

    }



    VariableParser variableParser = new VariableParser();

}