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

Add a system to change the start of the TCC numbering for CVC3. 

The CVC3 generator originally insured that the TCC numbering was always unqie
for a table.  Re-add this functionality.  Specifically, when building the walker,
add a parameter to its constructor to set its starting TCC number.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10712 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 78632af9

@CVC_checker/generate_cvc_grid.m

+1 −1
Original line number Diff line number Diff line
@@ -22,7 +22,7 @@ HGrid = ca.mcmaster.cas.tablularexpression.HierarchicalGrid 
TableBlock.convert_hierarchical_grid_to_java(grid.cells, HGrid.getSubHiearchy());

% generate the formulas for the main grid



gridGenerator = ca.mcmaster.cas.cvc3generator.HierarchicalGridCVC3Generator(var_def);

gridGenerator = ca.mcmaster.cas.cvc3generator.HierarchicalGridCVC3Generator(var_def, level);

code = char(ca.mcmaster.cas.tablularexpression.HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(HGrid, gridGenerator));

query = gridGenerator.getFinalQueries();

@CVC_checker/generate_file.m

+2 −2
Original line number Diff line number Diff line
@@ -28,12 +28,12 @@ new_code = ''; 
queries = [];

%generate grid 2

if size(object.data.Grid2.cells,2) > 1  

    [new_code,queries] = object.generate_cvc_grid(object.data.Grid2,0, inputs);

    [new_code,queries] = object.generate_cvc_grid(object.data.Grid2,1, inputs);

end

code = [code new_code];



if object.data.multi_mode == 0 && size(object.data.Grid1.cells,2) > 1

    [new_code,new_queries] = object.generate_cvc_grid(object.data.Grid1,size(queries,2), inputs);

    [new_code,new_queries] = object.generate_cvc_grid(object.data.Grid1,queries.size(), inputs);

    queries = [queries new_queries];

    code = [code new_code];

Matlab2SMT/src/main/java/ca/mcmaster/cas/cvc3generator/HierarchicalGridCVC3Generator.java

+2 −1
Original line number Diff line number Diff line
@@ -34,8 +34,9 @@ import org.apache.commons.lang3.StringUtils; 
 */

final public class HierarchicalGridCVC3Generator implements HierarchcialGridCheckerGenerator {



    public HierarchicalGridCVC3Generator(VariableParser variableDefinitions) {

    public HierarchicalGridCVC3Generator(VariableParser variableDefinitions, int queryCountStart) {

        m_variableDefinitions = variableDefinitions;

        m_currentTCC = queryCountStart;

    }



    private String generateQueryPrefix() {

Matlab2SMT/src/test/java/ca/mcmaster/cas/cvc3generator/HierarchicalGridCVC3GeneratorTest.java

+1 −1
Original line number Diff line number Diff line
@@ -52,7 +52,7 @@ public class HierarchicalGridCVC3GeneratorTest { 
        

        nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0"));



        String out = HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, new HierarchicalGridCVC3Generator(new VariableParser("x,z")));

        String out = HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, new HierarchicalGridCVC3Generator(new VariableParser("x,z"), 1));

        

        String expected = "ECHO \"begin1\";\n"+

"PUSH;\n"+