Commit fbbbd641 authored by Mark Lawford's avatar Mark Lawford
Browse files

Merge branch 'rename_to_jtet' into 'TableTool_javization' 

Rename the java components to jTET, and move the package to ca.mcscert.jtet

As discussed, do the various renames.  I'd like to do this once, so I want to get it checked off before causing further disturbances.
parents 83505e1f a8db2592

+TableBlock/convert_hierarchical_grid_to_java.m

+1 −1
Original line number Diff line number Diff line
@@ -13,7 +13,7 @@ 
function convert_hierarchical_grid_to_java(grid, java_grid)



for i=1:size(grid,2)

    new_cell = ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalCell;

    new_cell = ca.mcscert.jtet.tablularexpression.HierarchicalCell;

    

    old_cell = grid(i)

    new_cell.setContents(old_cell.cond_text)

.gitignore

+3 −3
Original line number Diff line number Diff line 
/Matlab2SMT/target/

/Matlab2SMT/gen/

/jTET/target/

/jTET/gen/

.idea/

.pvscontext

Matlab2SMT/Matlab2SMT.iml
 
/jTET/jtet.iml

@CVC_checker/CVC_checker.m

+2 −2
Original line number Diff line number Diff line
@@ -6,8 +6,8 @@ classdef CVC_checker 
        

        command = 'cvc3';

        data = [];

        generator = ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator();

        boolean_type = ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType();

        generator = ca.mcscert.jtet.expression.CVC3Generator();

        boolean_type = ca.mcscert.jtet.expression.BooleanVariableType();

        

    end

@CVC_checker/generate_cvc_grid.m

+3 −3
Original line number Diff line number Diff line
@@ -18,12 +18,12 @@ function [ code , query] = generate_cvc_grid( object, grid , level, var_def) 


% New Junk

% First build grid in java

HGrid = ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalGrid

HGrid = ca.mcscert.jtet.tablularexpression.HierarchicalGrid

TableBlock.convert_hierarchical_grid_to_java(grid.cells, HGrid.getSubHiearchy());

% generate the formulas for the main grid



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

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

gridGenerator = ca.mcscert.jtet.cvc3generator.HierarchicalGridCVC3Generator(var_def, level);

code = char(ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(HGrid, gridGenerator));

query = gridGenerator.getFinalQueries();

@GUI/smtlib_ext_call.m

+4 −4
Original line number Diff line number Diff line
@@ -17,16 +17,16 @@ if (~error) 
    inputs = TET.getInstance.getVariableParser.parseVariables(object.Data.function_inputs);

    vars = inputs.getVariables().values();



    HGrid = ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalGrid

    HGrid = ca.mcscert.jtet.tablularexpression.HierarchicalGrid

    TableBlock.convert_hierarchical_grid_to_java(object.Data.Grid2.cells, HGrid.getSubHiearchy());



    res = ca.mcmaster.cas.tabularexpressiontoolbox.smtlibchecker.CheckerRunner.RunZ3(HGrid, inputs);

    res = ca.mcscert.jtet.smtlibchecker.CheckerRunner.RunZ3(HGrid, inputs);



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

        HGrid = ca.mcmaster.cas.tabularexpressiontoolbox.tablularexpression.HierarchicalGrid

        HGrid = ca.mcscert.jtet.tablularexpression.HierarchicalGrid

        TableBlock.convert_hierarchical_grid_to_java(object.Data.Grid1.cells, HGrid.getSubHiearchy());



        res2 = ca.mcmaster.cas.tabularexpressiontoolbox.smtlibchecker.CheckerRunner.RunZ3(HGrid, inputs);

        res2 = ca.mcscert.jtet.smtlibchecker.CheckerRunner.RunZ3(HGrid, inputs);

        res.addAll(res2);

    end