Commit cbb12dd0 authored by Yanjun Jiang's avatar Yanjun Jiang Committed by Matthew Dawson
Browse files

Split the SMTLIBVariablesDeclarationGenerator from SMTLIBExpressionGenerator. 

This refactor is corresponding to split the VariablesDeclarationGenerator
interface from ExpressionGenerator interface commit.
parent e160bd1d

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

+1 −1
Original line number Diff line number Diff line
@@ -96,7 +96,7 @@ final public class CheckerRunner { 
        String GetValueRequestString = GetValueRequestBuilder.toString();



        try {

            String VarDef = new SMTLIBExpressionGenerator().GenerateVariablesDeclaration(vars);

            String VarDef = new SMTLIBVariablesDeclarationGenerator().GenerateVariablesDeclaration(vars);

            z3Input.write(VarDef);

            for(String query : queryGenerator.getFinalQueries()) {

                z3Input.write("(push 1)");

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

+3 −95
Original line number Diff line number Diff line
@@ -30,15 +30,13 @@ package ca.mcscert.jtet.smtlibchecker; 


import ca.mcscert.jtet.expression.*;



import java.util.HashSet;

import java.util.Map;

import java.util.Set;



/**

 *

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

 */

public class SMTLIBExpressionGenerator implements VariablesDeclarationGenerator, ExpressionGenerator {

public class SMTLIBExpressionGenerator implements ExpressionGenerator {

    public final static SMTLIBExpressionGenerator Generator = new SMTLIBExpressionGenerator();



    @Override

    public String GenerateUnaryOperation(UnaryOperation op, String expression, VariableType usedType) {

        return "(" + SMTLIBExpressionGenerator.GetUnaryOperationSymbolFor(op) + " " + expression + ")";  //To change body of implemented methods use File | Settings | File Templates.
@@ -62,96 +60,6 @@ public class SMTLIBExpressionGenerator implements VariablesDeclarationGenerator, 
        }

    }



    @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.

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

            ret.append("(declare-fun ")

               .append(var.outputName())

               .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.outputName())

                        .append("))\n");

            }

        }



        // Then generate the variable predicates.  This ensures any dependent variables are declared.

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

            if (var.type().subtypePredicate() != null) {

                ret.append("(assert ")

                        .append(var.type().subtypePredicate().getCheckerOutput(this, BooleanVariableType.Type))

                        .append(")\n");

            }

        }

        return ret.toString();

    }



    public static String GenerateVariableType(VariableType type) {

        if (type instanceof RealVariableType) {

            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() + ")");

        }

    }



    private static String GetBinaryOperationSymbolFor(BinaryOperation op) {

        switch (op) {

            case Addition:

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

0 → 100644
+136 −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.*;



import java.util.HashSet;

import java.util.Map;

import java.util.Set;



/**

 *

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

 */

public class SMTLIBVariablesDeclarationGenerator implements VariablesDeclarationGenerator {

    public final static SMTLIBVariablesDeclarationGenerator Generator = new SMTLIBVariablesDeclarationGenerator();



    @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.

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

            ret.append("(declare-fun ")

               .append(var.outputName())

               .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.outputName())

                        .append("))\n");

            }

        }



        // Then generate the variable predicates.  This ensures any dependent variables are declared.

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

            if (var.type().subtypePredicate() != null) {

                ret.append("(assert ")

                        .append(var.type().subtypePredicate().getCheckerOutput(SMTLIBExpressionGenerator.Generator, BooleanVariableType.Type))

                        .append(")\n");

            }

        }

        return ret.toString();

    }



    /**@deprecated

     * it is only public for unit tests, and will be made private eventually

     */

    public static String GenerateVariableType(VariableType type) {

        if (type instanceof RealVariableType) {

            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() + ")");

        }

    }

}

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.smtlibchecker.*;

import ca.mcscert.jtet.smtlibchecker.SMTLIBVariablesDeclarationGenerator;

import org.junit.Before;

import org.junit.Test;

import org.junit.runner.RunWith;
@@ -50,7 +50,7 @@ public class GenericVariablesDeclarationGeneratorTest { 
    @Parameters

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

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

                {new SMTLIBExpressionGenerator(),

                {new SMTLIBVariablesDeclarationGenerator(),

                        "(declare-fun x () Real)\n",

                        "(declare-fun new_x_name () Real)\n",

                        "(declare-fun x () Real)\n(assert (> x 0.0))\n",

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

+3 −3
Original line number Diff line number Diff line
@@ -8,7 +8,7 @@ import static org.hamcrest.CoreMatchers.is; 
import static org.junit.Assert.*;



import ca.mcscert.jtet.cvc3generator.CVC3VariablesDeclarationGenerator;

import ca.mcscert.jtet.smtlibchecker.SMTLIBExpressionGenerator;

import ca.mcscert.jtet.smtlibchecker.SMTLIBVariablesDeclarationGenerator;

import org.junit.Test;

import org.junit.runner.RunWith;

import org.junit.runners.JUnit4;
@@ -40,7 +40,7 @@ public class VariableTest { 
        VariablesDeclarationGenerator generator = new CVC3VariablesDeclarationGenerator();

        assertEquals(name+":REAL;\n", generator.GenerateVariablesDeclaration(variableCollection));



        generator = new SMTLIBExpressionGenerator();

        generator = new SMTLIBVariablesDeclarationGenerator();

        assertEquals("(declare-fun " +name+ " () Real)\n", generator.GenerateVariablesDeclaration(variableCollection));

    }
@@ -66,7 +66,7 @@ public class VariableTest { 


        assertThat(varDecl, is("var:REAL;\nASSERT (var > 0);\n"));



        generator = new SMTLIBExpressionGenerator();

        generator = new SMTLIBVariablesDeclarationGenerator();

        varDecl = generator.GenerateVariablesDeclaration(variableCollection);



        assertThat(varDecl, is("(declare-fun var () Real)\n(assert (> var 0.0))\n"));