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

Rename interface CheckerGenerator to ExpressionGenerator. 

To better reflect the job of CheckerGenerator, rename it to
ExpressionGenerator.  This prepares for the removal of the variable
declaration code.
parent 40b543ad

src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java

+1 −5
Original line number Diff line number Diff line
@@ -28,13 +28,9 @@ 
 */

package ca.mcscert.jtet.cvc3generator;



import ca.mcscert.jtet.expression.BinaryOperation;

import ca.mcscert.jtet.expression.*;

import ca.mcscert.jtet.expression.CheckerGeneratorSpy;

import ca.mcscert.jtet.expression.FixedPointVariableType;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.expression.BooleanVariableType;

import ca.mcscert.jtet.expression.CVC3Generator;

import ca.mcscert.jtet.tablularexpression.Cell;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridCheckerGenerator;

src/main/java/ca/mcscert/jtet/expression/CVC3Generator.java

+1 −1
Original line number Diff line number Diff line
@@ -16,7 +16,7 @@ import org.apache.commons.lang3.StringUtils; 
 *

 * @author matthew

 */

final public class CVC3Generator implements CheckerGenerator{

final public class CVC3Generator implements ExpressionGenerator {



    // For operations that don't have specific signed/unsigned representations, use this function.

    private static String GetIndifferentFixedPointFunctionFor(BinaryOperation op) {

src/main/java/ca/mcscert/jtet/expression/CheckerGenerator.java

deleted100644 → 0
+0 −16
Original line number Diff line number Diff line 
/*

 * To change this template, choose Tools | Templates

 * and open the template in the editor.

 */

package ca.mcscert.jtet.expression;



/**

 *

 * @author matthew

 */

public interface CheckerGenerator {

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

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

    public String GenerateLiteralValue(String value, VariableType requestedType);

    public String GenerateVariablesDeclaration(VariableCollection vars);

}

src/main/java/ca/mcscert/jtet/expression/CheckerGeneratorSpy.java

+11 −11
Original line number Diff line number Diff line
@@ -34,19 +34,19 @@ import java.util.Collections; 
import java.util.List;



/**

 * This inserts a spy between a given CheckerGenerator and the caller, recording all operations.

 * This inserts a spy between a given ExpressionGenerator and the caller, recording all operations.

 * <p>

 * This is useful if it is wanted to verify that all operations satisfy some property, for instance that all fixed point

 * operations do not under/overflow.

 * @author Matthew Dawson

 */

public class CheckerGeneratorSpy implements CheckerGenerator {

public class CheckerGeneratorSpy implements ExpressionGenerator {

    /**

     * Constructs the spy, using the given CheckerGenerator to generate the actual expressions.

     * @param checkerGenerator The CheckerGenerator to use to actually generate the expressions.

     * Constructs the spy, using the given ExpressionGenerator to generate the actual expressions.

     * @param expressionGenerator The ExpressionGenerator to use to actually generate the expressions.

     */

    public CheckerGeneratorSpy(CheckerGenerator checkerGenerator) {

        this.checkerGenerator = checkerGenerator;

    public CheckerGeneratorSpy(ExpressionGenerator expressionGenerator) {

        this.expressionGenerator = expressionGenerator;

    }



    /**
@@ -55,7 +55,7 @@ public class CheckerGeneratorSpy implements CheckerGenerator { 
    @Override

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

        m_spiedUnaryOps.add(new SpiedUnaryOp(op, expression, usedType));

        return checkerGenerator.GenerateUnaryOperation(op, expression, usedType);

        return expressionGenerator.GenerateUnaryOperation(op, expression, usedType);

    }



    /**
@@ -64,7 +64,7 @@ public class CheckerGeneratorSpy implements CheckerGenerator { 
    @Override

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

        m_spiedBinaryOps.add(new SpiedBinaryOp(lhsExp, op, rhsExp, usedType));

        return checkerGenerator.GenerateBinaryOperation(op, lhsExp, rhsExp, usedType);

        return expressionGenerator.GenerateBinaryOperation(op, lhsExp, rhsExp, usedType);

    }



    /**
@@ -74,7 +74,7 @@ public class CheckerGeneratorSpy implements CheckerGenerator { 
     */

    @Override

    public String GenerateLiteralValue(String value, VariableType requestedType) {

        return checkerGenerator.GenerateLiteralValue(value, requestedType);

        return expressionGenerator.GenerateLiteralValue(value, requestedType);

    }



    /**
@@ -84,7 +84,7 @@ public class CheckerGeneratorSpy implements CheckerGenerator { 
     */

    @Override

    public String GenerateVariablesDeclaration(VariableCollection vars) {

        return checkerGenerator.GenerateVariablesDeclaration(vars);

        return expressionGenerator.GenerateVariablesDeclaration(vars);

    }



    /**
@@ -169,7 +169,7 @@ public class CheckerGeneratorSpy implements CheckerGenerator { 
        }

    }



    private final CheckerGenerator checkerGenerator;

    private final ExpressionGenerator expressionGenerator;

    private final List<SpiedUnaryOp> m_spiedUnaryOps = new ArrayList<SpiedUnaryOp>();



    private final List<SpiedBinaryOp> m_spiedBinaryOps = new ArrayList<SpiedBinaryOp>();

src/main/java/ca/mcscert/jtet/expression/EventBGenerator.java

+1 −1
Original line number Diff line number Diff line
@@ -36,7 +36,7 @@ import java.util.Map; 
 *

 * @author Yanjun Jiang <jiangy76@mcmaster.ca>

 */

final public class EventBGenerator implements CheckerGenerator{

final public class EventBGenerator implements ExpressionGenerator {



    private static String GetInfixSymbolFor(BinaryOperation op) {

        switch (op) {