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

Rename the jTET package to ca.mcscert.jtet. 

As discussed, do the package rename now.  All MATLAB code is adjusted as necessary,
all java tests pass, and the quadratic example continues to typecheck, as
expected.
parent 3dbf1bdb

+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)

@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

TET.m

+1 −1
Original line number Diff line number Diff line
@@ -5,7 +5,7 @@ classdef (Sealed) TET < handle 
    %   globals used in the TET.



    properties (Access = private)

        variableParser = ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser

        variableParser = ca.mcscert.jtet.parsers.VariableParser

    end



    methods