cvc_check.m

%% cvc_check
% checks a table using cvc, parses results and returns them
%
% inputs:
%   object:cvc_checker - cvc_checker object
%
% outputs;
%   check:boolean - 0 if check fails, 1 if succeds
%   seqs:structure - if typecheck succeds then output contains
%       parsed output from cvc
% Author: Colin Eles elesc@mcmaster.ca
% Organization: McMaster Centre for Software Certification

function [ check, seqs ] = cvc_check( object )
%CVC_CHECK Summary of this function goes here
%   Detailed explanation goes here
    box = waitbar(0,'Generating Proof Script');

[filename, queries] = object.generate_file;

    waitbar(.10,box,'Running Proof');

    % run the cvc command
[status, result] = system(['cvc3 ' filename ' +model'])

% check return status for errors
if (status ~= 0)
    
    if (status == 127)
        msgbox('CVC3 command not found');
    else
        msgbox(['an error has occured!' char(10) result]);
    end
        check = 0;
        seqs = 'canceled';
        delete(box);
        return;
end

    waitbar(.70,box,'Parsing Results');

seqs = [];



% look for parse errors
fatal_exception = regexp(result,'*** Fatal exception');

if ~isempty(fatal_exception)
    msgbox(['CVC3 encountered a fatal exception' char(10) result],'Fatal Exception','error');
     check = 0;
         seqs = 'canceled';
         delete(box);
         return;
    
end


for i = 1:size(queries,2)
    asserts = [];

    % find results of individual queries, using regexp and notations in
    % output begin1 ... end1
    query_result = regexp(result,['(?<=begin' num2str(i) ').*(?=end' num2str(i) ')'],'match');
    
    invalid_found = regexp(char(query_result),'Invalid.|Unknown.');
    
    if ~isempty(invalid_found)
        % formula was found to be invalid
        % look for a counter example
        asserts =  regexp(char(query_result),'(?<=ASSERT[ ]*\()[^\n]*(?==)|(?<==)[^\n]*(?=\);)','match');

    
    if mod(i,2) == 1
        name = [filename '_' num2str(i) '_DIS'];
    else
        name = [filename '_' num2str(i) '_COM'];
    end    

        seqs = [seqs struct('id', '1234a', 'TCC', name, 'seq', queries(i), 'ce', {asserts})];
    end
    
    
    
end

if isempty(seqs)
    check = 1;
else
    check = 0;
end

    waitbar(1,box,'Deleting Proof Script');

    delete(box);


end