Commit 3fe4e5a0 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Get basic typecheck working with cvc3. 

Typechecking with cvc3 is now going.


git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_refactor@8776 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 8fc1c293

@CVC_checker/generate_cvc_grid.m

+20 −16
Original line number Diff line number Diff line
@@ -12,27 +12,30 @@ 
% 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( container , level, parent_cell, parent_cond)

if nargin == 2

    parent_cell = []

    parent_cond = ''

end



% generate the formulas for the main grid



parents = CVC_checker.find_parents(grid.cells(1));

if isempty(parents);

if isempty(parent_cond);

    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) ' => ('];

    disjoint = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parent_cond) ' => ('];

    complete = ['QUERY ' CVC_checker.matlab_to_cvc_syntax_translation(parent_cond) ' => ('];

end



for i=1:size(grid.cells,2)

    

for i=1:container.get_children_count(parent_cell)

    ith_cond = container.get_child_cell(parent_cell, i).get_matlab_string

  

    for j = i+1:size(grid.cells,2)

    for j = i+1:container.get_children_count(parent_cell)

        % 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)) ') )'];

        disjoint = [disjoint 'NOT ( (' CVC_checker.matlab_to_cvc_syntax_translation(ith_cond) ') AND (' CVC_checker.matlab_to_cvc_syntax_translation(char(container.get_child_cell(parent_cell, j).get_matlab_string)) ') )'];



        if j~= size(grid.cells,2)

        if j~= container.get_children_count(parent_cell)

             disjoint = [disjoint ' AND ' char(10)];



        end
@@ -43,13 +46,13 @@ for i=1:size(grid.cells,2) 
    

    

    

    complete = [complete '(' CVC_checker.matlab_to_cvc_syntax_translation(char(grid.cells(i).cond_text)) ')'];

    complete = [complete '(' CVC_checker.matlab_to_cvc_syntax_translation(ith_cond) ')'];

    

    if i < size(grid.cells,2) - 1

    if i < container.get_children_count(parent_cell)

        disjoint = [disjoint ' AND ' char(10)];

    end

    

    if i < size(grid.cells,2) 

    if i < container.get_children_count(parent_cell)

        complete = [complete ' OR '];

    end

end
@@ -63,9 +66,10 @@ code = [code 'ECHO "begin' num2str(level+2) '";' char(10) 'PUSH;' char(10) compl 






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

for i=1:container.get_children_count(parent_cell)

    child_cell = container.get_child_cell(parent_cell, i);

    if container.get_children_count(child_cell) ~= 0

        [new_code,new_queries] = CVC_checker.generate_cvc_grid(grid.cells(i).subgrid,level+2, child_cell);

        code = [code new_code];

        query = [query new_queries];

        level = size(query,2) - 2;

@CVC_checker/generate_file.m

+3 −3
Original line number Diff line number Diff line
@@ -34,12 +34,12 @@ end 
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);

if object.data.left_cond.length > 1  

    [new_code,queries] = CVC_checker.generate_cvc_grid(object.data.left_cond,0);

end

code = [code new_code];



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

if object.data.multi_mode == 0 && object.data.top_cond.length > 1

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

    queries = [queries new_queries];

    code = [code new_code];