Commit 31f8cc9a authored by Colin Eles's avatar Colin Eles
Browse files

latest update 

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6556 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 0ca04a93

@CVC_checker/cvc_check.m

+13 −13
Original line number Diff line number Diff line
@@ -27,18 +27,18 @@ end 
seqs = [];



% look for incompleteness, happens with non-linear artihmetic, ie.

% multiplication

incomplete = regexp(result,'CVC3 was incomplete in this example due to','match');

if ~isempty(incomplete)

    incomplete_reason = regexp(result,'(?<=CVC3 was incomplete in this example due to:\n)[^\n]*','match','once')

    msgbox(['CVC could not typecheck this table for the following reasons:' char(10) incomplete_reason]);

    

        check = 0;

        seqs = 'canceled';

        delete(box);

        return;

    

end

% % multiplication

% incomplete = regexp(result,'CVC3 was incomplete in this example due to','match');

% if ~isempty(incomplete)

%     incomplete_reason = regexp(result,'(?<=CVC3 was incomplete in this example due to:\n)[^\n]*','match','once')

%     msgbox(['CVC could not typecheck this table for the following reasons:' char(10) incomplete_reason]);

%     

%         check = 0;

%         seqs = 'canceled';

%         delete(box);

%         return;

%     

% end





for i = 1:size(queries,2)
@@ -48,7 +48,7 @@ for i = 1:size(queries,2) 
    % output begin1 ... end1

    query_result = regexp(result,['(?<=begin' num2str(i) ').*(?=end' num2str(i) ')'],'match');

    

    invalid_found = regexp(char(query_result),'Invalid.');

    invalid_found = regexp(char(query_result),'Invalid.|Unknown.');

    

    if ~isempty(invalid_found)

        % formula was found to be invalid