generate_cvc_grid.m

%% genereate_cvc_grid
% generate the queries for cvc for the inputted grid.
%
% 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
%   query:cell array - contains string representing both the disjoint and
%   complete without the comments, used for validation report.
% Author: Colin Eles elesc@mcmaster.ca
% Organization: McMaster Centre for Software Certification

function [ code , query] = generate_cvc_grid( object, grid , level, var_def)

% 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 ' object.matlab_to_cvc_syntax_translation(parents, var_def) ' => ('];
    complete = ['QUERY ' object.matlab_to_cvc_syntax_translation(parents, var_def) ' => ('];
end

for i=1:size(grid.cells,2)
    
  
    for j = i+1:size(grid.cells,2)
        % compare i to j
        disjoint = [disjoint 'NOT ( (' object.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text), var_def) ') AND (' object.matlab_to_cvc_syntax_translation(char(grid.cells(j).cond_text), var_def) ') )'];

        if j~= size(grid.cells,2)
             disjoint = [disjoint ' AND ' char(10)];

        end

    end
  % need to do pairwise disjointness
    % otherwise doesn't work
    
    
    
    complete = [complete '(' object.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text), var_def) ')'];
    
    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] = object.generate_cvc_grid(grid.cells(i).subgrid,level+2, var_def);
        code = [code new_code];
        query = [query new_queries];
        level = size(query,2) - 2;
    end

end

    




end