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

Rename/Remove the CheckerWalker's to have consistent names. 

The CheckerWalkers have grown in numbers, while duplicating their logic.  As
well, fix the naming to be consistent and easily identifiable.
parent 3073eefd

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

+5 −4
Original line number Diff line number Diff line
@@ -31,8 +31,9 @@ package ca.mcscert.jtet.cvc3generator; 
import ca.mcscert.jtet.expression.*;

import ca.mcscert.jtet.expression.ExpressionGeneratorSpy;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridBreadthFirstCheckerGenerator;

import ca.mcscert.jtet.tablularexpression.Cell;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridCheckerGenerator;





import java.util.ArrayList;

import java.util.ArrayDeque;
@@ -45,7 +46,7 @@ import org.apache.commons.lang3.StringUtils; 
 *

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

 */

final public class HierarchicalGridCVC3Generator implements HierarchicalGridCheckerGenerator {

final public class HierarchicalGridCVC3Generator implements HierarchicalGridBreadthFirstCheckerGenerator {



    public HierarchicalGridCVC3Generator(VariableCollection variableDefinitions, int queryCountStart) {

        m_variableDefinitions = variableDefinitions;
@@ -122,8 +123,8 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridChec 
    }



    @Override

    public void handleEdgeCell(Cell cell) {

        handleLeafCell(cell);

    public void handleEdgeCell(Cell inputCell) {

        handleLeafCell(inputCell);

    }



    @Override

src/main/java/ca/mcscert/jtet/salgenerator/HierarchicalGridSALGenerator.java

+2 −2
Original line number Diff line number Diff line
@@ -34,13 +34,13 @@ import ca.mcscert.jtet.expression.RealVariableType; 
import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.tablularexpression.Cell;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridCheckerGeneratorV2;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridDepthFirstCheckerGenerator;

import ca.mcscert.jtet.tablularexpression.TwoDimensionalGrid;



/**

 * Created by matthew on 6/3/14.

 */

public class HierarchicalGridSALGenerator implements HierarchicalGridCheckerGeneratorV2 {

public class HierarchicalGridSALGenerator implements HierarchicalGridDepthFirstCheckerGenerator {



    public HierarchicalGridSALGenerator(VariableCollection variableDefinitions, TwoDimensionalGrid outputGrid)

    {

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

+2 −2
Original line number Diff line number Diff line
@@ -34,8 +34,8 @@ import ca.mcscert.jtet.smtlibchecker.antlr.SMTLibOutParserBaseListener; 
import ca.mcscert.jtet.smtlibchecker.antlr.SMTLibOutParserLexer;

import ca.mcscert.jtet.smtlibchecker.antlr.SMTLibOutParserListener;

import ca.mcscert.jtet.smtlibchecker.antlr.SMTLibOutParserParser;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridCheckerWalkerGenerator;

import ca.mcscert.jtet.tablularexpression.HierarchicalGrid;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridBreadthFirstCheckerWalkerGenerator;

import org.antlr.v4.runtime.ANTLRInputStream;

import org.antlr.v4.runtime.CommonTokenStream;

import org.antlr.v4.runtime.misc.NotNull;
@@ -64,7 +64,7 @@ final public class CheckerRunner { 


        // Get the queries

        HierarchicalGridSMTLIBGenerator queryGenerator = new HierarchicalGridSMTLIBGenerator(vars);

        HierarchicalGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, queryGenerator);

        HierarchicalGridBreadthFirstCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, queryGenerator);



        // Start Z3

        ProcessBuilder pb;

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

+4 −4
Original line number Diff line number Diff line
@@ -31,8 +31,8 @@ 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.tablularexpression.HierarchicalGridBreadthFirstCheckerGenerator;

import ca.mcscert.jtet.tablularexpression.Cell;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridCheckerGenerator;

import org.apache.commons.lang3.StringUtils;



import java.util.ArrayDeque;
@@ -44,7 +44,7 @@ import java.util.List; 
 *

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

 */

final public class HierarchicalGridSMTLIBGenerator implements HierarchicalGridCheckerGenerator {

final public class HierarchicalGridSMTLIBGenerator implements HierarchicalGridBreadthFirstCheckerGenerator {



    public HierarchicalGridSMTLIBGenerator(VariableCollection variableDefinitions) {

        m_variableDefinitions = variableDefinitions;
@@ -122,8 +122,8 @@ final public class HierarchicalGridSMTLIBGenerator implements HierarchicalGridCh 
    }



    @Override

    public void handleEdgeCell(Cell cell) {

        handleLeafCell(cell);

    public void handleEdgeCell(Cell inputCell) {

        handleLeafCell(inputCell);

    }



    @Override

src/main/java/ca/mcscert/jtet/tablularexpression/HierarchicalGridCheckerGenerator.java→src/main/java/ca/mcscert/jtet/tablularexpression/HierarchicalGridBreadthFirstCheckerGenerator.java

+8 −6
Original line number Diff line number Diff line
@@ -28,16 +28,18 @@ 
 */

package ca.mcscert.jtet.tablularexpression;



import java.util.List;



/**

 *

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

 */

public interface HierarchicalGridCheckerGenerator {

    void descendIntoGridFromCell(Cell cell);

public interface HierarchicalGridBreadthFirstCheckerGenerator {

    void descendIntoGridFromCell(Cell inputCell);

    void ascendFromGrid();



    void handleLeafCell(Cell cell);

    void handleEdgeCell(Cell cell);

    void handleLeafCell(Cell inputCell);

    void handleEdgeCell(Cell inputCell);



    String getFinalString();

}