+TETTests/run.m

+function test_results = run
+%RUN Runs TET test suite
+%   Runs all the tests in TET, returning the result.
+TETLoadjTET
+
+path = mfilename('fullpath');
+path = [path(1:size(path, 2)-13) 'Tests'];
+test_results = run(matlab.unittest.TestSuite.fromFolder(path));
+end
+

+TableBlock/convert_hierarchical_grid_to_java.m

+%% convert_hierarchical_grid_to_java
+% generates a java version fo the hiearchcial grid
+%
+% inputs:
+%   grid:Grid - grid to convert
+%   java_grid:List<HierarchicalCell> - place to put changed cells.
+%
+% outputs;
+%   none
+% Author: Matthew Dawson matthew@mjdsystems.ca
+% Organization: McMaster Centre for Software Certification
+
+function convert_hierarchical_grid_to_java(grid, java_grid)
+
+for i=1:size(grid,2)
+    new_cell = ca.mcscert.jtet.tablularexpression.HierarchicalCell;
+    
+    old_cell = grid(i)
+    new_cell.setContents(old_cell.cond_text)
+    
+    if ~isempty(old_cell.subgrid)
+        TableBlock.convert_hierarchical_grid_to_java(old_cell.subgrid.cells, new_cell.getSubHiearchy())
+    end
+    java_grid.add(new_cell)
+end
+
+end
+

+TableBlock/convert_table_to_java_table.m

+function outtable = convert_table_to_java_table( intable )
+%CONVERT_TABLE_TO_JAVA_TABLE Converts a given table to jTET's representation
+%   This function converts a table from TET's internal representation to
+%   jTET's representation, ready for use against any of jTET's tools.
+
+    outputVariables = java.util.Arrays.asList([ca.mcscert.jtet.expression.Variable('output', ca.mcscert.jtet.expression.RealVariableType())]);
+    vc = ca.mcscert.jtet.expression.VariableCollection(TET.getInstance.getVariableParser.parseVariables(intable.function_inputs), ca.mcscert.jtet.expression.PartialVariableCollection(outputVariables));
+    outtable = ca.mcscert.jtet.tabularexpression.Table(intable.function_name, vc);
+
+end
+

+TableBlock/convert_twodimensional_grid_to_java.m

+%% convert_hierarchical_grid_to_java
+% generates a java version fo the hiearchcial grid
+%
+% inputs:
+%   grid:Grid - grid to convert
+%   java_grid:List<HierarchicalCell> - place to put changed cells.
+%
+% outputs;
+%   none
+% Author: Matthew Dawson matthew@mjdsystems.ca
+% Organization: McMaster Centre for Software Certification
+
+function convert_twodimensional_grid_to_java(grid, java_grid)
+
+% Pre-set the x size.
+java_grid.setSize(size(grid.Grid1.cells, 2), 1)
+
+TableBlock.convert_twodimensional_grid_to_java_real(grid, grid.Grid2.cells, grid.Grid1.cells, java_grid, 0)
+
+end
+

+TableBlock/convert_twodimensional_grid_to_java_real.m

+%% convert_hierarchical_grid_to_java
+% generates a java version fo the hiearchcial grid
+%
+% inputs:
+%   grid:Grid - grid to convert
+%   java_grid:List<HierarchicalCell> - place to put changed cells.
+%
+% outputs;
+%   none
+% Author: Matthew Dawson matthew@mjdsystems.ca
+% Organization: McMaster Centre for Software Certification
+
+function current_index = convert_twodimensional_grid_to_java_real(grid, left_grid, top_gird, java_grid, current_index)
+
+for i=1:size(left_grid,2)
+    % If we are not a leaf node on the left, descend:
+    if ~isempty(old_cell.subgrid)
+        current_index = TableBlock.convert_twodimensional_grid_to_java_real(grid, left_grid(i).subgrid.cells, top_grid, java_grid, current_index)
+    else % Otherwise, we are the reference cell for the 2d grid.  So pull results out.
+        java_grid.resize(java_grid.sizeX(), current_index + 1)
+        for j=1:size(top_grid, 2)
+            java_grid.get(j, current_index).setContents(grid.search_return(top_grid(j), left_grid(i)).result_text);
+        end
+        current_index=current_index+1;
+    end
+end
+
+end
+

.gitignore

+/jTET/jtet-1.0-SNAPSHOT-jar-with-dependencies.jar
+*~

@CVC_checker/CVC_checker.m

@@ -6,16 +6,7 @@ classdef CVC_checker
         
         command = 'cvc3';
         data = [];
-        
-    end
-    
-    
-    methods(Static)
-        
-        [ code , query] = generate_cvc_grid( grid , level);
-        [ code ] = find_parents( grid );
-        cvc_string = matlab_to_cvc_syntax_translation(matlab_string);
-        [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type );
+        generator = ca.mcscert.jtet.cvc3generator.CVC3VariablesDeclarationGenerator();
         
     end
     

@CVC_checker/cvc_check.m

@@ -56,7 +56,7 @@ if ~isempty(fatal_exception)
 end
 
 
-for i = 1:size(queries,2)
+for i = 1:queries.size()
     asserts = [];
 
     % find results of individual queries, using regexp and notations in
@@ -77,7 +77,7 @@ for i = 1:size(queries,2)
         name = [filename '_' num2str(i) '_COM'];
     end    
 
-        seqs = [seqs struct('id', '1234a', 'TCC', name, 'seq', queries(i), 'ce', {asserts})];
+        seqs = [seqs struct('id', '1234a', 'TCC', name, 'seq', queries.get(i-1), 'ce', {asserts})];
     end
     
     

@CVC_checker/cvc_parse_result.m

-function [ output_args ] = cvc_parse_result( input_args )
-%CVC_PARSE_RESULT Summary of this function goes here
-%   Detailed explanation goes here
-
-
-end
-

@CVC_checker/find_parents.m

-%% find_parents
-% function will find all the parents of a cell, used to determine what
-% preconditions must be true.
-%
-% inputs:
-%   cell:Cell - cell to find the parents of
-%
-% outputs;
-%   code:string - string of conjunction of all parent cells.
-% Author: Colin Eles elesc@mcmaster.ca
-% Organization: McMaster Centre for Software Certification
-
-function [ code ] = find_parents( cell )
-% assumption, initial input will be grid we want to find parents for not
-%  cell itself
-
-code = '';
-if isempty(cell)
-    % current cell is empty
-    code = '';
-else
-    if isempty(cell.parent_grid.parent_cell)
-        % no parent cell
-        
-    else
-        % there is a parent cell
-        top = char(CVC_checker.find_parents(cell.parent_grid.parent_cell));
-        code = char(cell.parent_grid.parent_cell.cond_text);
-        if isempty(top);
-            % there were no more above this cell
-            
-        else
-            % there were more above this cell
-            code = [code ' AND ' top];
-        end
-        
-        
-    end
-    
-    
-end
-
-
-
-
-end
-

@CVC_checker/generate_cvc_grid.m

@@ -4,6 +4,8 @@
 % inputs:
 %   grid:Grid - grid to generate conditions for.
 %   level:int - count of the queries generated.
+%   var_def:VariableParser - Parsed input of the variables, available in
+%   the MATLAB2SMT java package.
 %
 % outputs;
 %   code:string - string representing code to generate including comments
@@ -12,68 +14,17 @@
 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
 
-function [ code , query] = generate_cvc_grid( grid , level)
+function [ code , query] = generate_cvc_grid( object, grid , level, var_def)
 
+% New Junk
+% First build grid in java
+HGrid = ca.mcscert.jtet.tablularexpression.HierarchicalGrid
+TableBlock.convert_hierarchical_grid_to_java(grid.cells, HGrid.getSubHiearchy());
 % generate the formulas for the main grid
 
-parents = CVC_checker.find_parents(grid.cells(1));
-if isempty(parents);
-    disjoint = 'QUERY (';
-    complete = 'QUERY (';
-else
-    disjoint = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parents) ' => ('];
-    complete = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parents) ' => ('];
-end
-
-for i=1:size(grid.cells,2)
-    
-  
-    for j = i+1:size(grid.cells,2)
-        % compare i to j
-        disjoint = [disjoint 'NOT ( (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text)) ') AND (' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(j).cond_text)) ') )'];
-
-        if j~= size(grid.cells,2)
-             disjoint = [disjoint ' AND ' char(10)];
-
-        end
-
-    end
-  % need to do pairwise disjointness
-    % otherwise doesn't work
-    
-    
-    
-    complete = [complete '(' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text)) ')'];
-    
-    if i < size(grid.cells,2) - 1
-        disjoint = [disjoint ' AND ' char(10)];
-    end
-    
-    if i < size(grid.cells,2) 
-        complete = [complete ' OR '];
-    end
-end
-disjoint = [disjoint ');'];
-complete = [complete ');'];
-
-query = [{disjoint} {complete}];
-
-code = ['ECHO "begin' num2str(level+1) '";' char(10) 'PUSH;'  char(10) disjoint char(10) 'POP;' char(10) 'ECHO "end' num2str(level+1) '";' char(10)];
-code = [code 'ECHO "begin' num2str(level+2) '";' char(10) 'PUSH;' char(10) complete  char(10) 'POP;' char(10) 'ECHO "end' num2str(level+2) '";' char(10)];
-
-
-
-for i=1:size(grid.cells,2)
-    if ~isempty(grid.cells(i).subgrid)
-        [new_code,new_queries] = CVC_checker.generate_cvc_grid(grid.cells(i).subgrid,level+2);
-        code = [code new_code];
-        query = [query new_queries];
-        level = size(query,2) - 2;
-    end
-
-end
-
-    
+gridGenerator = ca.mcscert.jtet.cvc3generator.HierarchicalGridCVC3Generator(var_def, level);
+code = char(ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(HGrid, gridGenerator));
+query = gridGenerator.getFinalQueries();
 
 
 

@CVC_checker/generate_file.m

@@ -19,15 +19,8 @@ function_name = char(function_names{1}(1));
 
 code = [];
 % output the input variables
-inputs = EMLGenerator.parse_inputs(object.data.function_inputs);
-for i = 1:size(inputs,2)
-    if size(inputs{i},2) > 1
-        cvc_type = CVC_checker.pvs_to_cvc_subtypes(inputs{i}(2));
-    else
-        cvc_type = 'REAL';
-    end
-    code = [code char(inputs{i}(1)) ':' char(cvc_type) ';' char(10)];
-end
+inputs = TET.getInstance.getVariableParser.parseVariables(object.data.function_inputs);
+code = char(object.generator.GenerateVariablesDeclaration(inputs));
 
 
 % call the recursive function to generate the queries
@@ -35,13 +28,13 @@ new_code = '';
 queries = [];
 %generate grid 2
 if size(object.data.Grid2.cells,2) > 1  
-    [new_code,queries] = CVC_checker.generate_cvc_grid(object.data.Grid2,0);
+    [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] = CVC_checker.generate_cvc_grid(object.data.Grid1,size(queries,2));
-    queries = [queries new_queries];
+    [new_code,new_queries] = object.generate_cvc_grid(object.data.Grid1,queries.size(), inputs);
+    queries.addAll(new_queries);
     code = [code new_code];
 
 end   

@CVC_checker/matlab_to_cvc_syntax_translation.m

-%% matlab_to_cvc_syntax_translation
-%translate matlab syntax to cvc syntax,
-% will be added to in the future
-% will only work for functions in the prelude
-%
-% inputs:
-%   object:cvc_checker - cvc_checker object
-%   matlab_string:string - string to be converted from matlab
-%       syntax to cvc
-% outputs;
-%   cvc_string:string - string converted to cvc syntax.
-% Author: Colin Eles elesc@mcmaster.ca
-% Organization: McMaster Centre for Software Certification
-function cvc_string = matlab_to_cvc_syntax_translation(matlab_string)
-
-s = [matlab_string(1,:)];
-for j = 2:size(matlab_string,1)
-   s = [s ' ' matlab_string(j,:)];
-end
-matlab_string = s;
-
-cvc_string = regexprep(matlab_string,'&&',' AND ');
-cvc_string = regexprep(cvc_string,'~(?!=)',' NOT ');
-cvc_string = regexprep(cvc_string,'~=',' /= ');
-cvc_string = regexprep(cvc_string,'==',' = ');
-cvc_string = regexprep(cvc_string,'\|\|',' OR ');
-cvc_string = regexprep(cvc_string,'ceil','ceiling');
-
-floats = regexp(cvc_string,'[0-9]*\.[0-9]*','match');
-for i=1:size(floats,2)
-   cvc_string = regexprep(cvc_string,floats{i},['(' strtrim(num2str(rats(eval(floats{i})))) ')'] );
-end
-
-end
-
-
-
-

@CVC_checker/pvs_to_cvc_subtypes.m

-%% pvs_to_cvc_subtypes
-% converts types of the pvs syntax to cvc3 syntax. the syntax for doing
-% typing in the two languages is slightly different so we need to write
-% this function to translate between them.
-%
-% inputs:
-%   pvs_type:string - a string of a pvs type
-% outputs;
-%   cvc_type:string - a string of the cvc type.
-% Author: Colin Eles elesc@mcmaster.ca
-% Organization: McMaster Centre for Software Certification
-
-function [ cvc_type ] = pvs_to_cvc_subtypes( pvs_type )
-%PVS_TO_CVC_SUBTYPES Summary of this function goes here
-%   Detailed explanation goes here
-
-
-
-
-%pvs_type is parsed
-string = char(pvs_type);
-
-% change cases
-string = regexprep(string,'real','REAL');
-string = regexprep(string,'Real','REAL');
-string = regexprep(string,'int','INT');
-string = regexprep(string,'Int','INT');
-string = regexprep(string,'bool','BOOLEAN');
-string = regexprep(string,'Bool','BOOLEAN');
-string = regexprep(string,'BOOL[^EAN]','BOOLEAN');
-
-% remove brackets
-string_no_brack = regexp(string,'(?<=\{)[^\n]*(?=\})','match');
-if isempty(string_no_brack)
-    
-    cvc_type = {string};
-    return
-end
-
-split_at_pipe = regexp(char(string_no_brack),'\|','split');
-if (size(split_at_pipe,2) ~= 2)
-    %something strange happened
-    cvc_type = {string};
-    return;
-end
-
-new_type = ['SUBTYPE( LAMBDA (' char(split_at_pipe{1}) '): ' char(split_at_pipe{2}) ')'];
-cvc_type = {new_type};
-
-    
-
-
-end
-

@EMLGenerator/generate_preamble.m

@@ -13,11 +13,14 @@ function code = generate_preamble(object)
 code = [];
 function_name = EMLGenerator.parse_inputs(object.data.function_name);
 %generate input list
-parsed_input = EMLGenerator.parse_inputs(object.data.function_inputs);
+inputs = TET.getInstance.getVariableParser.parseVariables(object.data.function_inputs);
+parsed_input = inputs.m_variables.values();
+input_iter = parsed_input.iterator();
 input = [];
-for i= 1:size(parsed_input,2)
-    input = [input char(parsed_input{i}(1))];
-    if i ~= size(parsed_input,2)
+while input_iter.hasNext()
+    var = input_iter.next();
+    input = [input char(var.name())];
+    if input_iter.hasNext()
         input = [input ','];
     end
 end

@GUI/GUI.m

@@ -64,6 +64,7 @@ classdef GUI < handle
         multi_opt_out = [];
         prover_opt_pvs = [];
         prover_opt_cvc = [];
+        prover_opt_smtlib = [];
         version = '0.7.3';
         undo_man = [];
         undo_opt = [];
@@ -72,6 +73,7 @@ classdef GUI < handle
         default_prover = [];
         PVS_const = 1;
         CVC_const = 2;
+        SMTLIB_const = 3;
         
     end
     

@GUI/check_inputs.m

@@ -11,7 +11,9 @@
 % Author: Colin Eles elesc@mcmaster.ca
 % Organization: McMaster Centre for Software Certification
 function error = check_inputs(object)
-parsed_input = EMLGenerator.parse_inputs(get(object.function_inputs_control,'string'));
+%parsed_input = EMLGenerator.parse_inputs(get(object.function_inputs_control,'string'));
+%TODO FIX THIS!
+parsed_input = [];
 error = [];
 for i=1:size(parsed_input,2)
     if(size(parsed_input{i},2) == 2)

@GUI/check_matlab_syntax_condition.m

@@ -15,7 +15,9 @@
 % Organization: McMaster Centre for Software Certification
 function error = check_matlab_syntax_condition(object,string,result)
 % split the list of inputs to get inputs seperatly
-
+%TODO FIX THIS!
+error = [];
+return ;
 parsed_input = EMLGenerator.parse_inputs(get(object.function_inputs_control,'string'));
 check_string = [];
 

@GUI/init.m

@@ -161,6 +161,7 @@ uimenu(checkmenu,'Label','Typecheck','Accelerator','t','Callback',@(src,event)ty
 prover_menu = uimenu(checkmenu,'Label','Default Prover');
 object.prover_opt_cvc = uimenu(prover_menu,'Label','CVC3','Callback',@(src,event)prover_select_call(object,src,event));
 object.prover_opt_pvs = uimenu(prover_menu,'Label','PVS','Callback',@(src,event)prover_select_call(object,src,event));
+object.prover_opt_smtlib = uimenu(prover_menu,'Label','Z3','Callback',@(src,event)prover_select_call(object,src,event));
 uimenu(checkmenu,'Label', 'Syntax Check','Callback',@(src,event)check_call(object,src,event));
 
 
@@ -173,6 +174,8 @@ uimenu(checkmenu,'Label','PVS Check Status','Callback',@(src,event)prf_file_call
 uimenu(checkmenu,'Label','PVS Generate file','Callback',@(src,event)pvs_file_call(object,src,event));
 uimenu(checkmenu,'Label','PVS Typecheck SimTypes','Callback',@(src,event)pvs_ext_call_sim(object,src,event));
 
+uimenu(checkmenu,'Label','Z3 Typecheck','Separator','on','Callback',@(src,event)smtlib_ext_call(object,src,event));
+
 uimenu(helpmenu,'Label','Product Help','Callback',@(src,event)help_call(object,src,event));
 uimenu(helpmenu,'Label','About Tabular Expression Toolbox','Callback',@(src,event)about_call(object,src,event));
 

@GUI/prover_select_call.m

@@ -3,8 +3,10 @@ label = get(src,'Label');
 % determine which label the user clicked on
 if strcmp(label,'CVC3')
     object.default_prover = object.CVC_const;
-else
+elseif strcmp(label,'PVS')
     object.default_prover = object.PVS_const;
+else
+    object.default_prover = object.SMTLIB_const;
 end
 
 object.update_prover_check_status;