Commit 5a0a4664 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Make sure enumerated types are only emitted once. 

Make sure enumerated types are only emitted once, even when there is more
then one variable declared with the type.  Also fix the generators so they
actually ensure this.

Also, CVC3Generator got some cleanup around the relevant code.
parent 1159bc39

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

+5 −2
Original line number Diff line number Diff line
@@ -206,12 +206,13 @@ final public class CVC3Generator implements CheckerGenerator{ 
        // First generate all the enumeration types.

        for(Variable var : vars.values()) {

            if (var.type() instanceof EnumerationVariableType && !emittedEnumerations.contains(var.type())) {

                EnumerationVariableType enumType = (EnumerationVariableType) var.type();

                ret.append("DATATYPE\n  ")

                        .append(((EnumerationVariableType) var.type()).name())

                        .append((enumType).name())

                        .append(" = ");



                boolean firstValue = false;

                for(String enumValue : ((EnumerationVariableType) var.type()).enumerationValues()) {

                for(String enumValue : enumType.enumerationValues()) {

                    if (firstValue == true) {

                        ret.append(" | ");

                    }
@@ -219,6 +220,8 @@ final public class CVC3Generator implements CheckerGenerator{ 
                    ret.append(enumValue);

                }

                ret.append("\nEND;\n");



                emittedEnumerations.add(enumType);

            }

        }

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

+2 −0
Original line number Diff line number Diff line
@@ -92,6 +92,8 @@ public class SMTLIBGenerator implements CheckerGenerator { 
                            .append(")");

                }

                ret.append("))\n");



                emittedEnumerations.add(enumType);

            }

        }

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

+31 −9
Original line number Diff line number Diff line
@@ -25,10 +25,7 @@ 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 java.util.*;



import static org.junit.Assert.*;
@@ -51,13 +48,24 @@ public class GenericVariableDeclarationGeneratorTest { 
                                "(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"

                                "(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 x () MyEnum)\n" +

                                "(assert (isMyEnum x))\n" +

                                "(declare-fun y () MyEnum)\n" +

                                "(assert (isMyEnum y))\n"

                },

                {new CVC3Generator(),

                        "x:REAL;\n",

                        "x:BITVECTOR(8);\n",

                        "x:BITVECTOR(8);\n",

                        "DATATYPE\n  MyEnum = e1 | e2 | e3\nEND;\nx:MyEnum;\n"

                        "DATATYPE\n  MyEnum = e1 | e2 | e3\nEND;\nx:MyEnum;\n",

                        "DATATYPE\n  MyEnum = e1 | e2 | e3\nEND;\nx:MyEnum;\ny:MyEnum;\n"

                }

        });

    }
@@ -74,7 +82,10 @@ public class GenericVariableDeclarationGeneratorTest { 
    public String UnsignedFixedPointExpectedOutput;



    @Parameter(value = 4)

    public String EnumerationExpectedOutput;

    public String SingleVariableSingleEnumerationExpectedOutput;



    @Parameter(value = 5)

    public String MultipleVariableSingleEnumerationExpectedOutput;



    @Test

    public void RealTest() {
@@ -102,9 +113,20 @@ public class GenericVariableDeclarationGeneratorTest { 


    @Test

    public void SingleVariableSingleEnumerationTest() {

        if (EnumerationExpectedOutput != null) {

        if (SingleVariableSingleEnumerationExpectedOutput != null) {

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

            assertEquals(EnumerationExpectedOutput, generator.GenerateVariablesDeclaration(vars));

            assertEquals(SingleVariableSingleEnumerationExpectedOutput, generator.GenerateVariablesDeclaration(vars));

        }

    }



    // This ensures that the enumeration definition is only emitted once.  Other variable generations don't have this,

    // as they don't emit type information.

    @Test

    public void MultipleVariableSingleEnumerationTest() {

        if (MultipleVariableSingleEnumerationExpectedOutput != null) {

            VariableCollection vars = variableParser.parseVariables("x:MyEnum, y:MyEnum");



            assertEquals(MultipleVariableSingleEnumerationExpectedOutput, generator.GenerateVariablesDeclaration(vars));

        }

    }