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

Rename SMTLIBGenerator to SMTLIBExpressionGenerator. 

This commit is used to keep the changes history clean so that the
modification is easy to see.
parent 94f6f45a

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

+1 −2
Original line number Diff line number Diff line
@@ -28,7 +28,6 @@ 
 */

package ca.mcscert.jtet.smtlibchecker;



import ca.mcscert.jtet.expression.SMTLIBGenerator;

import ca.mcscert.jtet.expression.Variable;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.smtlibchecker.antlr.SMTLibOutParserBaseListener;
@@ -97,7 +96,7 @@ final public class CheckerRunner { 
        String GetValueRequestString = GetValueRequestBuilder.toString();



        try {

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

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

            z3Input.write(VarDef);

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

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

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

+1 −2
Original line number Diff line number Diff line
@@ -31,7 +31,6 @@ package ca.mcscert.jtet.smtlibchecker; 
import ca.mcscert.jtet.expression.BooleanVariableType;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.expression.SMTLIBGenerator;

import ca.mcscert.jtet.tablularexpression.Cell;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridCheckerGenerator;

import org.apache.commons.lang3.StringUtils;
@@ -169,5 +168,5 @@ final public class HierarchicalGridSMTLIBGenerator implements HierarchicalGridCh 


    // To fix properly.

    VariableCollection m_variableDefinitions;

    SMTLIBGenerator m_CVC3Generator = new SMTLIBGenerator();

    SMTLIBExpressionGenerator m_CVC3Generator = new SMTLIBExpressionGenerator();

}

src/main/java/ca/mcscert/jtet/expression/SMTLIBGenerator.java→src/main/java/ca/mcscert/jtet/smtlibchecker/SMTLIBExpressionGenerator.java

+6 −4
Original line number Diff line number Diff line
@@ -26,7 +26,9 @@ 
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE

 * POSSIBILITY OF SUCH DAMAGE.

 */

package ca.mcscert.jtet.expression;

package ca.mcscert.jtet.smtlibchecker;



import ca.mcscert.jtet.expression.*;



import java.util.HashSet;

import java.util.Map;
@@ -36,15 +38,15 @@ import java.util.Set; 
 *

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

 */

public class SMTLIBGenerator implements VariablesDeclarationGenerator, ExpressionGenerator {

public class SMTLIBExpressionGenerator implements VariablesDeclarationGenerator, ExpressionGenerator {

    @Override

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

        return "(" + SMTLIBGenerator.GetUnaryOperationSymbolFor(op) + " " + expression + ")";  //To change body of implemented methods use File | Settings | File Templates.

        return "(" + SMTLIBExpressionGenerator.GetUnaryOperationSymbolFor(op) + " " + expression + ")";  //To change body of implemented methods use File | Settings | File Templates.

    }



    @Override

    public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType) {

        return "(" + SMTLIBGenerator.GetBinaryOperationSymbolFor(op) + " " + lhsExp + " " + rhsExp + ")";

        return "(" + SMTLIBExpressionGenerator.GetBinaryOperationSymbolFor(op) + " " + lhsExp + " " + rhsExp + ")";

    }



    @Override

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

+2 −1
Original line number Diff line number Diff line
@@ -31,6 +31,7 @@ package ca.mcscert.jtet.expression; 
import ca.mcscert.jtet.cvc3generator.CVC3ExpressionGenerator;

import ca.mcscert.jtet.parsers.PVSSimpleParser;

import ca.mcscert.jtet.parsers.VariableParser;

import ca.mcscert.jtet.smtlibchecker.SMTLIBExpressionGenerator;

import org.junit.Before;

import org.junit.Test;

import org.junit.runner.RunWith;
@@ -51,7 +52,7 @@ public class EnumerationVariableTypeGenerationTest { 
    @Parameters

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

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

                {new SMTLIBGenerator(),

                {new SMTLIBExpressionGenerator(),

                        "(= x e1)",

                        "(distinct x e1)",

                },

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

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



import ca.mcscert.jtet.cvc3generator.CVC3ExpressionGenerator;

import ca.mcscert.jtet.smtlibchecker.SMTLIBExpressionGenerator;

import ca.mcscert.jtet.parsers.PVSSimpleParser;

import ca.mcscert.jtet.parsers.VariableParser;

import org.junit.Test;
@@ -50,7 +51,7 @@ public class GenericOperationGeneratorTest { 
    @Parameters

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

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

                {new SMTLIBGenerator(),

                {new SMTLIBExpressionGenerator(),

                        "(=> (or (= (* x 5.0) (/ 1.0 (- 4.0))) (or (and (> x (+ 8.0 3.0)) (< 9.0 (- x 2.0))) (or (>= x 12.0) (or (not (<= 34.0 (- x))) (> 5.0 4.0))))) (distinct x 5.0))",

                        null,

                        null},